author | wenzelm |
Wed, 08 Nov 2006 13:48:29 +0100 | |
changeset 21243 | afffe1f72143 |
parent 21216 | 1c8580913738 |
permissions | -rw-r--r-- |
15511 | 1 |
(* Title: HOL/Lattices.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
*) |
|
5 |
||
6 |
header {* Lattices via Locales *} |
|
7 |
||
8 |
theory Lattice_Locales |
|
21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
9 |
imports Orderings |
15511 | 10 |
begin |
11 |
||
12 |
subsection{* Lattices *} |
|
13 |
||
14 |
text{* This theory of lattice locales only defines binary sup and inf |
|
15 |
operations. The extension to finite sets is done in theory @{text |
|
16 |
Finite_Set}. In the longer term it may be better to define arbitrary |
|
17 |
sups and infs via @{text THE}. *} |
|
18 |
||
19 |
locale lower_semilattice = partial_order + |
|
20 |
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |
|
21 |
assumes inf_le1: "x \<sqinter> y \<sqsubseteq> x" and inf_le2: "x \<sqinter> y \<sqsubseteq> y" |
|
22 |
and inf_least: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z" |
|
23 |
||
24 |
locale upper_semilattice = partial_order + |
|
25 |
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
|
26 |
assumes sup_ge1: "x \<sqsubseteq> x \<squnion> y" and sup_ge2: "y \<sqsubseteq> x \<squnion> y" |
|
27 |
and sup_greatest: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x" |
|
28 |
||
29 |
locale lattice = lower_semilattice + upper_semilattice |
|
30 |
||
31 |
lemma (in lower_semilattice) inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)" |
|
32 |
by(blast intro: antisym inf_le1 inf_le2 inf_least) |
|
33 |
||
34 |
lemma (in upper_semilattice) sup_commute: "(x \<squnion> y) = (y \<squnion> x)" |
|
35 |
by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest) |
|
36 |
||
37 |
lemma (in lower_semilattice) inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
|
38 |
by(blast intro: antisym inf_le1 inf_le2 inf_least trans del:refl) |
|
39 |
||
40 |
lemma (in upper_semilattice) sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
|
41 |
by(blast intro!: antisym sup_ge1 sup_ge2 intro: sup_greatest trans del:refl) |
|
42 |
||
43 |
lemma (in lower_semilattice) inf_idem[simp]: "x \<sqinter> x = x" |
|
44 |
by(blast intro: antisym inf_le1 inf_le2 inf_least refl) |
|
45 |
||
46 |
lemma (in upper_semilattice) sup_idem[simp]: "x \<squnion> x = x" |
|
47 |
by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl) |
|
48 |
||
15791 | 49 |
lemma (in lower_semilattice) inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" |
50 |
by (simp add: inf_assoc[symmetric]) |
|
51 |
||
52 |
lemma (in upper_semilattice) sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y" |
|
53 |
by (simp add: sup_assoc[symmetric]) |
|
54 |
||
15511 | 55 |
lemma (in lattice) inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x" |
56 |
by(blast intro: antisym inf_le1 inf_least sup_ge1) |
|
57 |
||
58 |
lemma (in lattice) sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x" |
|
59 |
by(blast intro: antisym sup_ge1 sup_greatest inf_le1) |
|
60 |
||
61 |
lemma (in lower_semilattice) inf_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" |
|
62 |
by(blast intro: antisym inf_le1 inf_least refl) |
|
63 |
||
64 |
lemma (in upper_semilattice) sup_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" |
|
65 |
by(blast intro: antisym sup_ge2 sup_greatest refl) |
|
66 |
||
15524
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15511
diff
changeset
|
67 |
|
21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
68 |
lemma (in lower_semilattice) less_eq_inf_conv [simp]: |
15524
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15511
diff
changeset
|
69 |
"x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)" |
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15511
diff
changeset
|
70 |
by(blast intro: antisym inf_le1 inf_le2 inf_least refl trans) |
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15511
diff
changeset
|
71 |
|
21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
72 |
lemmas (in lower_semilattice) below_inf_conv = less_eq_inf_conv |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
73 |
-- {* a duplicate for backward compatibility *} |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
74 |
|
15524
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15511
diff
changeset
|
75 |
lemma (in upper_semilattice) above_sup_conv[simp]: |
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15511
diff
changeset
|
76 |
"x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)" |
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15511
diff
changeset
|
77 |
by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl trans) |
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15511
diff
changeset
|
78 |
|
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15511
diff
changeset
|
79 |
|
15511 | 80 |
text{* Towards distributivity: if you have one of them, you have them all. *} |
81 |
||
82 |
lemma (in lattice) distrib_imp1: |
|
83 |
assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
|
84 |
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
|
85 |
proof- |
|
86 |
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb) |
|
87 |
also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc) |
|
88 |
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" |
|
89 |
by(simp add:inf_sup_absorb inf_commute) |
|
90 |
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D) |
|
91 |
finally show ?thesis . |
|
92 |
qed |
|
93 |
||
94 |
lemma (in lattice) distrib_imp2: |
|
95 |
assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
|
96 |
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
|
97 |
proof- |
|
98 |
have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb) |
|
99 |
also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc) |
|
100 |
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" |
|
101 |
by(simp add:sup_inf_absorb sup_commute) |
|
102 |
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D) |
|
103 |
finally show ?thesis . |
|
104 |
qed |
|
105 |
||
106 |
text{* A package of rewrite rules for deciding equivalence wrt ACI: *} |
|
107 |
||
108 |
lemma (in lower_semilattice) inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)" |
|
109 |
proof - |
|
110 |
have "x \<sqinter> (y \<sqinter> z) = (y \<sqinter> z) \<sqinter> x" by (simp only: inf_commute) |
|
111 |
also have "... = y \<sqinter> (z \<sqinter> x)" by (simp only: inf_assoc) |
|
112 |
also have "z \<sqinter> x = x \<sqinter> z" by (simp only: inf_commute) |
|
15524
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15511
diff
changeset
|
113 |
finally(back_subst) show ?thesis . |
15511 | 114 |
qed |
115 |
||
116 |
lemma (in upper_semilattice) sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)" |
|
117 |
proof - |
|
118 |
have "x \<squnion> (y \<squnion> z) = (y \<squnion> z) \<squnion> x" by (simp only: sup_commute) |
|
119 |
also have "... = y \<squnion> (z \<squnion> x)" by (simp only: sup_assoc) |
|
120 |
also have "z \<squnion> x = x \<squnion> z" by (simp only: sup_commute) |
|
15524
2ef571f80a55
Moved oderings from HOL into the new Orderings.thy
nipkow
parents:
15511
diff
changeset
|
121 |
finally(back_subst) show ?thesis . |
15511 | 122 |
qed |
123 |
||
124 |
lemma (in lower_semilattice) inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" |
|
125 |
proof - |
|
126 |
have "x \<sqinter> (x \<sqinter> y) = (x \<sqinter> x) \<sqinter> y" by(simp only:inf_assoc) |
|
127 |
also have "\<dots> = x \<sqinter> y" by(simp) |
|
128 |
finally show ?thesis . |
|
129 |
qed |
|
130 |
||
131 |
lemma (in upper_semilattice) sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y" |
|
132 |
proof - |
|
133 |
have "x \<squnion> (x \<squnion> y) = (x \<squnion> x) \<squnion> y" by(simp only:sup_assoc) |
|
134 |
also have "\<dots> = x \<squnion> y" by(simp) |
|
135 |
finally show ?thesis . |
|
136 |
qed |
|
137 |
||
138 |
||
139 |
lemmas (in lower_semilattice) inf_ACI = |
|
140 |
inf_commute inf_assoc inf_left_commute inf_left_idem |
|
141 |
||
142 |
lemmas (in upper_semilattice) sup_ACI = |
|
143 |
sup_commute sup_assoc sup_left_commute sup_left_idem |
|
144 |
||
145 |
lemmas (in lattice) ACI = inf_ACI sup_ACI |
|
146 |
||
147 |
||
148 |
subsection{* Distributive lattices *} |
|
149 |
||
150 |
locale distrib_lattice = lattice + |
|
151 |
assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
|
152 |
||
153 |
lemma (in distrib_lattice) sup_inf_distrib2: |
|
154 |
"(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" |
|
155 |
by(simp add:ACI sup_inf_distrib1) |
|
156 |
||
157 |
lemma (in distrib_lattice) inf_sup_distrib1: |
|
158 |
"x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
|
159 |
by(rule distrib_imp2[OF sup_inf_distrib1]) |
|
160 |
||
161 |
lemma (in distrib_lattice) inf_sup_distrib2: |
|
162 |
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" |
|
163 |
by(simp add:ACI inf_sup_distrib1) |
|
164 |
||
165 |
lemmas (in distrib_lattice) distrib = |
|
166 |
sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 |
|
167 |
||
168 |
||
21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
169 |
subsection {* Least value operator and min/max -- properties *} |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
170 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
171 |
(*FIXME: derive more of the min/max laws generically via semilattices*) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
172 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
173 |
lemma LeastI2_order: |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
174 |
"[| P (x::'a::order); |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
175 |
!!y. P y ==> x <= y; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
176 |
!!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |] |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
177 |
==> Q (Least P)" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
178 |
apply (unfold Least_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
179 |
apply (rule theI2) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
180 |
apply (blast intro: order_antisym)+ |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
181 |
done |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
182 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
183 |
lemma Least_equality: |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
184 |
"[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
185 |
apply (simp add: Least_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
186 |
apply (rule the_equality) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
187 |
apply (auto intro!: order_antisym) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
188 |
done |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
189 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
190 |
lemma min_leastL: "(!!x. least <= x) ==> min least x = least" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
191 |
by (simp add: min_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
192 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
193 |
lemma max_leastL: "(!!x. least <= x) ==> max least x = x" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
194 |
by (simp add: max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
195 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
196 |
lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
197 |
apply (simp add: min_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
198 |
apply (blast intro: order_antisym) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
199 |
done |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
200 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
201 |
lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
202 |
apply (simp add: max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
203 |
apply (blast intro: order_antisym) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
204 |
done |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
205 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
206 |
lemma min_of_mono: |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
207 |
"(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
208 |
by (simp add: min_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
209 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
210 |
lemma max_of_mono: |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
211 |
"(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
212 |
by (simp add: max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
213 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
214 |
text{* Instantiate locales: *} |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
215 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
216 |
interpretation min_max: |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
217 |
lower_semilattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"] |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
218 |
apply unfold_locales |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
219 |
apply(simp add:min_def linorder_not_le order_less_imp_le) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
220 |
apply(simp add:min_def linorder_not_le order_less_imp_le) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
221 |
apply(simp add:min_def linorder_not_le order_less_imp_le) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
222 |
done |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
223 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
224 |
interpretation min_max: |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
225 |
upper_semilattice["op \<le>" "op <" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"] |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
226 |
apply unfold_locales |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
227 |
apply(simp add: max_def linorder_not_le order_less_imp_le) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
228 |
apply(simp add: max_def linorder_not_le order_less_imp_le) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
229 |
apply(simp add: max_def linorder_not_le order_less_imp_le) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
230 |
done |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
231 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
232 |
interpretation min_max: |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
233 |
lattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"] |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
234 |
by unfold_locales |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
235 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
236 |
interpretation min_max: |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
237 |
distrib_lattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"] |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
238 |
apply unfold_locales |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
239 |
apply(rule_tac x=x and y=y in linorder_le_cases) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
240 |
apply(rule_tac x=x and y=z in linorder_le_cases) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
241 |
apply(rule_tac x=y and y=z in linorder_le_cases) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
242 |
apply(simp add:min_def max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
243 |
apply(simp add:min_def max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
244 |
apply(rule_tac x=y and y=z in linorder_le_cases) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
245 |
apply(simp add:min_def max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
246 |
apply(simp add:min_def max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
247 |
apply(rule_tac x=x and y=z in linorder_le_cases) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
248 |
apply(rule_tac x=y and y=z in linorder_le_cases) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
249 |
apply(simp add:min_def max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
250 |
apply(simp add:min_def max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
251 |
apply(rule_tac x=y and y=z in linorder_le_cases) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
252 |
apply(simp add:min_def max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
253 |
apply(simp add:min_def max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
254 |
done |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
255 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
256 |
lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
257 |
apply(simp add:max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
258 |
apply (insert linorder_linear) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
259 |
apply (blast intro: order_trans) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
260 |
done |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
261 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
262 |
lemmas le_maxI1 = min_max.sup_ge1 |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
263 |
lemmas le_maxI2 = min_max.sup_ge2 |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
264 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
265 |
lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
266 |
apply (simp add: max_def order_le_less) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
267 |
apply (insert linorder_less_linear) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
268 |
apply (blast intro: order_less_trans) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
269 |
done |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
270 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
271 |
lemma max_less_iff_conj [simp]: |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
272 |
"!!z::'a::linorder. (max x y < z) = (x < z & y < z)" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
273 |
apply (simp add: order_le_less max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
274 |
apply (insert linorder_less_linear) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
275 |
apply (blast intro: order_less_trans) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
276 |
done |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
277 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
278 |
lemma min_less_iff_conj [simp]: |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
279 |
"!!z::'a::linorder. (z < min x y) = (z < x & z < y)" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
280 |
apply (simp add: order_le_less min_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
281 |
apply (insert linorder_less_linear) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
282 |
apply (blast intro: order_less_trans) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
283 |
done |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
284 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
285 |
lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
286 |
apply (simp add: min_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
287 |
apply (insert linorder_linear) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
288 |
apply (blast intro: order_trans) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
289 |
done |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
290 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
291 |
lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z | y < z)" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
292 |
apply (simp add: min_def order_le_less) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
293 |
apply (insert linorder_less_linear) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
294 |
apply (blast intro: order_less_trans) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
295 |
done |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
296 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
297 |
lemmas max_ac = min_max.sup_assoc min_max.sup_commute |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
298 |
mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute] |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
299 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
300 |
lemmas min_ac = min_max.inf_assoc min_max.inf_commute |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
301 |
mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute] |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
302 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
303 |
lemma split_min: |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
304 |
"P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
305 |
by (simp add: min_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
306 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
307 |
lemma split_max: |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
308 |
"P (max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))" |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
309 |
by (simp add: max_def) |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
310 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
311 |
text {* ML legacy bindings *} |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
312 |
|
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
313 |
ML {* |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
314 |
val Least_def = thm "Least_def"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
315 |
val Least_equality = thm "Least_equality"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
316 |
val min_def = thm "min_def"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
317 |
val min_of_mono = thm "min_of_mono"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
318 |
val max_def = thm "max_def"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
319 |
val max_of_mono = thm "max_of_mono"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
320 |
val min_leastL = thm "min_leastL"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
321 |
val max_leastL = thm "max_leastL"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
322 |
val min_leastR = thm "min_leastR"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
323 |
val max_leastR = thm "max_leastR"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
324 |
val le_max_iff_disj = thm "le_max_iff_disj"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
325 |
val le_maxI1 = thm "le_maxI1"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
326 |
val le_maxI2 = thm "le_maxI2"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
327 |
val less_max_iff_disj = thm "less_max_iff_disj"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
328 |
val max_less_iff_conj = thm "max_less_iff_conj"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
329 |
val min_less_iff_conj = thm "min_less_iff_conj"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
330 |
val min_le_iff_disj = thm "min_le_iff_disj"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
331 |
val min_less_iff_disj = thm "min_less_iff_disj"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
332 |
val split_min = thm "split_min"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
333 |
val split_max = thm "split_max"; |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
334 |
*} |
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
15791
diff
changeset
|
335 |
|
15511 | 336 |
end |