author | haftmann |
Fri, 09 Mar 2007 08:45:50 +0100 | |
changeset 22422 | ee19cdb07528 |
parent 21734 | 283461c15fa7 |
permissions | -rw-r--r-- |
14738 | 1 |
(* Title: HOL/LOrder.thy |
2 |
ID: $Id$ |
|
3 |
Author: Steven Obua, TU Muenchen |
|
21734 | 4 |
|
5 |
FIXME integrate properly with lattice locales |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
6 |
- get rid of the implicit there-is-a-meet/join but require explicit ops. |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
7 |
- abandone semilorder axclasses, instead turn lattice locales into classes |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
8 |
- rename meet/join to inf/sup in all theorems |
14738 | 9 |
*) |
10 |
||
21312 | 11 |
header "Lattice Orders" |
14738 | 12 |
|
15131 | 13 |
theory LOrder |
21249 | 14 |
imports Lattices |
15131 | 15 |
begin |
14738 | 16 |
|
21312 | 17 |
text {* The theory of lattices developed here is taken from |
18 |
\cite{Birkhoff79}. *} |
|
14738 | 19 |
|
20 |
constdefs |
|
21 |
is_meet :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" |
|
22 |
"is_meet m == ! a b x. m a b \<le> a \<and> m a b \<le> b \<and> (x \<le> a \<and> x \<le> b \<longrightarrow> x \<le> m a b)" |
|
23 |
is_join :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" |
|
24 |
"is_join j == ! a b x. a \<le> j a b \<and> b \<le> j a b \<and> (a \<le> x \<and> b \<le> x \<longrightarrow> j a b \<le> x)" |
|
25 |
||
26 |
lemma is_meet_unique: |
|
27 |
assumes "is_meet u" "is_meet v" shows "u = v" |
|
28 |
proof - |
|
29 |
{ |
|
30 |
fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
31 |
assume a: "is_meet a" |
|
32 |
assume b: "is_meet b" |
|
33 |
{ |
|
34 |
fix x y |
|
35 |
let ?za = "a x y" |
|
36 |
let ?zb = "b x y" |
|
37 |
from a have za_le: "?za <= x & ?za <= y" by (auto simp add: is_meet_def) |
|
38 |
with b have "?za <= ?zb" by (auto simp add: is_meet_def) |
|
39 |
} |
|
40 |
} |
|
41 |
note f_le = this |
|
42 |
show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le) |
|
43 |
qed |
|
44 |
||
45 |
lemma is_join_unique: |
|
46 |
assumes "is_join u" "is_join v" shows "u = v" |
|
47 |
proof - |
|
48 |
{ |
|
49 |
fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
50 |
assume a: "is_join a" |
|
51 |
assume b: "is_join b" |
|
52 |
{ |
|
53 |
fix x y |
|
54 |
let ?za = "a x y" |
|
55 |
let ?zb = "b x y" |
|
56 |
from a have za_le: "x <= ?za & y <= ?za" by (auto simp add: is_join_def) |
|
57 |
with b have "?zb <= ?za" by (auto simp add: is_join_def) |
|
58 |
} |
|
59 |
} |
|
60 |
note f_le = this |
|
61 |
show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le) |
|
62 |
qed |
|
63 |
||
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
64 |
lemma is_meet_inf: "is_meet (inf \<Colon> 'a\<Colon>lower_semilattice \<Rightarrow> 'a \<Rightarrow> 'a)" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
65 |
unfolding is_meet_def by auto |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
66 |
|
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
67 |
lemma is_join_sup: "is_join (sup \<Colon> 'a\<Colon>upper_semilattice \<Rightarrow> 'a \<Rightarrow> 'a)" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
68 |
unfolding is_join_def by auto |
14738 | 69 |
|
70 |
axclass meet_semilorder < order |
|
71 |
meet_exists: "? m. is_meet m" |
|
72 |
||
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
73 |
axclass join_semilorder < order |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
74 |
join_exists: "? j. is_join j" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
75 |
|
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
76 |
axclass lorder < meet_semilorder, join_semilorder |
14738 | 77 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
78 |
definition |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
79 |
inf :: "('a::meet_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a" where |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
80 |
"inf = (THE m. is_meet m)" |
14738 | 81 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
82 |
definition |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
83 |
sup :: "('a::join_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a" where |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
84 |
"sup = (THE j. is_join j)" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
85 |
|
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
86 |
lemma is_meet_meet: "is_meet (inf::'a \<Rightarrow> 'a \<Rightarrow> ('a::meet_semilorder))" |
14738 | 87 |
proof - |
88 |
from meet_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_meet k" .. |
|
89 |
with is_meet_unique[of _ k] show ?thesis |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
90 |
by (simp add: inf_def theI [of is_meet]) |
14738 | 91 |
qed |
92 |
||
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
93 |
lemma is_join_join: "is_join (sup::'a \<Rightarrow> 'a \<Rightarrow> ('a::join_semilorder))" |
14738 | 94 |
proof - |
95 |
from join_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_join k" .. |
|
96 |
with is_join_unique[of _ k] show ?thesis |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
97 |
by (simp add: sup_def theI[of is_join]) |
14738 | 98 |
qed |
99 |
||
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
100 |
lemma meet_unique: "(is_meet m) = (m = inf)" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
101 |
by (insert is_meet_meet, auto simp add: is_meet_unique) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
102 |
|
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
103 |
lemma join_unique: "(is_join j) = (j = sup)" |
14738 | 104 |
by (insert is_join_join, auto simp add: is_join_unique) |
105 |
||
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
106 |
lemma inf_unique: "(is_meet m) = (m = (Lattices.inf \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>lower_semilattice))" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
107 |
by (insert is_meet_inf, auto simp add: is_meet_unique) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
108 |
|
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
109 |
lemma sup_unique: "(is_join j) = (j = (Lattices.sup \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>upper_semilattice))" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
110 |
by (insert is_join_sup, auto simp add: is_join_unique) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
111 |
|
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
112 |
interpretation inf_semilat: |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
113 |
lower_semilattice ["op \<le> \<Colon> 'a\<Colon>meet_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" inf] |
21380 | 114 |
proof unfold_locales |
21733 | 115 |
fix x y z :: "'a\<Colon>meet_semilorder" |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
116 |
from is_meet_meet have "is_meet inf" by blast |
21380 | 117 |
note meet = this is_meet_def |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
118 |
from meet show "inf x y \<le> x" by blast |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
119 |
from meet show "inf x y \<le> y" by blast |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
120 |
from meet show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z" by blast |
21733 | 121 |
qed |
122 |
||
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
123 |
interpretation sup_semilat: |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
124 |
upper_semilattice ["op \<le> \<Colon> 'a\<Colon>join_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" sup] |
21733 | 125 |
proof unfold_locales |
126 |
fix x y z :: "'a\<Colon>join_semilorder" |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
127 |
from is_join_join have "is_join sup" by blast |
21380 | 128 |
note join = this is_join_def |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
129 |
from join show "x \<le> sup x y" by blast |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
130 |
from join show "y \<le> sup x y" by blast |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
131 |
from join show "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> sup x y \<le> z" by blast |
21380 | 132 |
qed |
133 |
||
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
134 |
interpretation inf_sup_lat: |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
135 |
lattice ["op \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" inf sup] |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
136 |
by unfold_locales |
14738 | 137 |
|
138 |
lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))" |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
139 |
by (auto simp add: is_meet_def min_def) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
140 |
lemma is_join_max: "is_join (max::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
141 |
by (auto simp add: is_join_def max_def) |
14738 | 142 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
143 |
instance linorder \<subseteq> lorder |
14738 | 144 |
proof |
145 |
from is_meet_min show "? (m::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_meet m" by auto |
|
146 |
from is_join_max show "? (j::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_join j" by auto |
|
147 |
qed |
|
148 |
||
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
149 |
lemma meet_min: "inf = (min \<Colon> 'a\<Colon>{linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
150 |
by (simp add: is_meet_meet is_meet_min is_meet_unique) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
151 |
lemma join_max: "sup = (max \<Colon> 'a\<Colon>{linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
152 |
by (simp add: is_join_join is_join_max is_join_unique) |
14738 | 153 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
154 |
lemmas [rule del] = sup_semilat.antisym_intro inf_semilat.antisym_intro |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
155 |
sup_semilat.le_supE inf_semilat.le_infE |
14738 | 156 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
157 |
lemmas inf_le1 = inf_semilat.inf_le1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
158 |
lemmas inf_le2 = inf_semilat.inf_le2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
159 |
lemmas le_infI [rule del] = inf_semilat.le_infI |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
160 |
(*intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes*) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
161 |
lemmas sup_ge1 = sup_semilat.sup_ge1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
162 |
lemmas sup_ge2 = sup_semilat.sup_ge2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
163 |
lemmas le_supI [rule del] = sup_semilat.le_supI |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
164 |
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
165 |
lemmas le_inf_iff = inf_semilat.le_inf_iff |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
166 |
lemmas ge_sup_conv = sup_semilat.ge_sup_conv |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
167 |
lemmas inf_idem = inf_semilat.inf_idem |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
168 |
lemmas sup_idem = sup_semilat.sup_idem |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
169 |
lemmas inf_commute = inf_semilat.inf_commute |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
170 |
lemmas sup_commute = sup_semilat.sup_commute |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
171 |
lemmas le_infI1 [rule del] = inf_semilat.le_infI1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
172 |
lemmas le_infI2 [rule del] = inf_semilat.le_infI2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
173 |
lemmas le_supI1 [rule del] = sup_semilat.le_supI1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
174 |
lemmas le_supI2 [rule del] = sup_semilat.le_supI2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
175 |
lemmas inf_assoc = inf_semilat.inf_assoc |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
176 |
lemmas sup_assoc = sup_semilat.sup_assoc |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
177 |
lemmas inf_left_commute = inf_semilat.inf_left_commute |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
178 |
lemmas inf_left_idem = inf_semilat.inf_left_idem |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
179 |
lemmas sup_left_commute = sup_semilat.sup_left_commute |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
180 |
lemmas sup_left_idem= sup_semilat.sup_left_idem |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
181 |
lemmas inf_aci = inf_assoc inf_commute inf_left_commute inf_left_idem |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
182 |
lemmas sup_aci = sup_assoc sup_commute sup_left_commute sup_left_idem |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
183 |
lemmas le_iff_inf = inf_semilat.le_iff_inf |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
184 |
lemmas le_iff_sup = sup_semilat.le_iff_sup |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
185 |
lemmas sup_absorb2 = sup_semilat.sup_absorb2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
186 |
lemmas sup_absorb1 = sup_semilat.sup_absorb1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
187 |
lemmas inf_absorb1 = inf_semilat.inf_absorb1 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
188 |
lemmas inf_absorb2 = inf_semilat.inf_absorb2 |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
189 |
lemmas inf_sup_absorb = inf_sup_lat.inf_sup_absorb |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
190 |
lemmas sup_inf_absorb = inf_sup_lat.sup_inf_absorb |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
191 |
lemmas distrib_sup_le = inf_sup_lat.distrib_sup_le |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21734
diff
changeset
|
192 |
lemmas distrib_inf_le = inf_sup_lat.distrib_inf_le |
14738 | 193 |
|
15131 | 194 |
end |