author | wenzelm |
Sun, 10 Mar 2019 23:23:03 +0100 | |
changeset 69895 | 6b03a8cf092d |
parent 69861 | 62e47f06d22c |
child 77138 | c8597292cd41 |
permissions | -rw-r--r-- |
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
50573
diff
changeset
|
1 |
(* Title: HOL/Library/Product_Order.thy |
44006 | 2 |
Author: Brian Huffman |
3 |
*) |
|
4 |
||
60500 | 5 |
section \<open>Pointwise order on product types\<close> |
44006 | 6 |
|
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
50573
diff
changeset
|
7 |
theory Product_Order |
63972 | 8 |
imports Product_Plus |
44006 | 9 |
begin |
10 |
||
60500 | 11 |
subsection \<open>Pointwise ordering\<close> |
44006 | 12 |
|
13 |
instantiation prod :: (ord, ord) ord |
|
14 |
begin |
|
15 |
||
16 |
definition |
|
17 |
"x \<le> y \<longleftrightarrow> fst x \<le> fst y \<and> snd x \<le> snd y" |
|
18 |
||
19 |
definition |
|
20 |
"(x::'a \<times> 'b) < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" |
|
21 |
||
22 |
instance .. |
|
23 |
||
24 |
end |
|
25 |
||
26 |
lemma fst_mono: "x \<le> y \<Longrightarrow> fst x \<le> fst y" |
|
27 |
unfolding less_eq_prod_def by simp |
|
28 |
||
29 |
lemma snd_mono: "x \<le> y \<Longrightarrow> snd x \<le> snd y" |
|
30 |
unfolding less_eq_prod_def by simp |
|
31 |
||
32 |
lemma Pair_mono: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> (x, y) \<le> (x', y')" |
|
33 |
unfolding less_eq_prod_def by simp |
|
34 |
||
35 |
lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d" |
|
36 |
unfolding less_eq_prod_def by simp |
|
37 |
||
38 |
instance prod :: (preorder, preorder) preorder |
|
39 |
proof |
|
40 |
fix x y z :: "'a \<times> 'b" |
|
41 |
show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" |
|
42 |
by (rule less_prod_def) |
|
43 |
show "x \<le> x" |
|
44 |
unfolding less_eq_prod_def |
|
45 |
by fast |
|
46 |
assume "x \<le> y" and "y \<le> z" thus "x \<le> z" |
|
47 |
unfolding less_eq_prod_def |
|
48 |
by (fast elim: order_trans) |
|
49 |
qed |
|
50 |
||
51 |
instance prod :: (order, order) order |
|
60679 | 52 |
by standard auto |
44006 | 53 |
|
54 |
||
60500 | 55 |
subsection \<open>Binary infimum and supremum\<close> |
44006 | 56 |
|
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
57 |
instantiation prod :: (inf, inf) inf |
44006 | 58 |
begin |
59 |
||
60679 | 60 |
definition "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))" |
44006 | 61 |
|
62 |
lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)" |
|
63 |
unfolding inf_prod_def by simp |
|
64 |
||
65 |
lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)" |
|
66 |
unfolding inf_prod_def by simp |
|
67 |
||
68 |
lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)" |
|
69 |
unfolding inf_prod_def by simp |
|
70 |
||
60679 | 71 |
instance .. |
72 |
||
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
73 |
end |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
74 |
|
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
75 |
instance prod :: (semilattice_inf, semilattice_inf) semilattice_inf |
60679 | 76 |
by standard auto |
44006 | 77 |
|
78 |
||
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
79 |
instantiation prod :: (sup, sup) sup |
44006 | 80 |
begin |
81 |
||
82 |
definition |
|
83 |
"sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))" |
|
84 |
||
85 |
lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)" |
|
86 |
unfolding sup_prod_def by simp |
|
87 |
||
88 |
lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)" |
|
89 |
unfolding sup_prod_def by simp |
|
90 |
||
91 |
lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)" |
|
92 |
unfolding sup_prod_def by simp |
|
93 |
||
60679 | 94 |
instance .. |
95 |
||
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
96 |
end |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
97 |
|
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
98 |
instance prod :: (semilattice_sup, semilattice_sup) semilattice_sup |
60679 | 99 |
by standard auto |
44006 | 100 |
|
101 |
instance prod :: (lattice, lattice) lattice .. |
|
102 |
||
103 |
instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice |
|
60679 | 104 |
by standard (auto simp add: sup_inf_distrib1) |
44006 | 105 |
|
106 |
||
60500 | 107 |
subsection \<open>Top and bottom elements\<close> |
44006 | 108 |
|
109 |
instantiation prod :: (top, top) top |
|
110 |
begin |
|
111 |
||
112 |
definition |
|
113 |
"top = (top, top)" |
|
114 |
||
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51542
diff
changeset
|
115 |
instance .. |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51542
diff
changeset
|
116 |
|
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51542
diff
changeset
|
117 |
end |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51542
diff
changeset
|
118 |
|
44006 | 119 |
lemma fst_top [simp]: "fst top = top" |
120 |
unfolding top_prod_def by simp |
|
121 |
||
122 |
lemma snd_top [simp]: "snd top = top" |
|
123 |
unfolding top_prod_def by simp |
|
124 |
||
125 |
lemma Pair_top_top: "(top, top) = top" |
|
126 |
unfolding top_prod_def by simp |
|
127 |
||
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51542
diff
changeset
|
128 |
instance prod :: (order_top, order_top) order_top |
60679 | 129 |
by standard (auto simp add: top_prod_def) |
44006 | 130 |
|
131 |
instantiation prod :: (bot, bot) bot |
|
132 |
begin |
|
133 |
||
134 |
definition |
|
135 |
"bot = (bot, bot)" |
|
136 |
||
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51542
diff
changeset
|
137 |
instance .. |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51542
diff
changeset
|
138 |
|
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51542
diff
changeset
|
139 |
end |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51542
diff
changeset
|
140 |
|
44006 | 141 |
lemma fst_bot [simp]: "fst bot = bot" |
142 |
unfolding bot_prod_def by simp |
|
143 |
||
144 |
lemma snd_bot [simp]: "snd bot = bot" |
|
145 |
unfolding bot_prod_def by simp |
|
146 |
||
147 |
lemma Pair_bot_bot: "(bot, bot) = bot" |
|
148 |
unfolding bot_prod_def by simp |
|
149 |
||
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51542
diff
changeset
|
150 |
instance prod :: (order_bot, order_bot) order_bot |
60679 | 151 |
by standard (auto simp add: bot_prod_def) |
44006 | 152 |
|
153 |
instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice .. |
|
154 |
||
155 |
instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra |
|
62053 | 156 |
by standard (auto simp add: prod_eqI diff_eq) |
44006 | 157 |
|
158 |
||
60500 | 159 |
subsection \<open>Complete lattice operations\<close> |
44006 | 160 |
|
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
161 |
instantiation prod :: (Inf, Inf) Inf |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
162 |
begin |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
163 |
|
69260
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
67829
diff
changeset
|
164 |
definition "Inf A = (INF x\<in>A. fst x, INF x\<in>A. snd x)" |
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
165 |
|
60679 | 166 |
instance .. |
167 |
||
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
168 |
end |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
169 |
|
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
170 |
instantiation prod :: (Sup, Sup) Sup |
44006 | 171 |
begin |
172 |
||
69260
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
67829
diff
changeset
|
173 |
definition "Sup A = (SUP x\<in>A. fst x, SUP x\<in>A. snd x)" |
44006 | 174 |
|
60679 | 175 |
instance .. |
176 |
||
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
177 |
end |
44006 | 178 |
|
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
179 |
instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice) |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
180 |
conditionally_complete_lattice |
60679 | 181 |
by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def |
62053 | 182 |
intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+ |
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
183 |
|
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
52729
diff
changeset
|
184 |
instance prod :: (complete_lattice, complete_lattice) complete_lattice |
60679 | 185 |
by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def |
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51542
diff
changeset
|
186 |
INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def) |
44006 | 187 |
|
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
188 |
lemma fst_Inf: "fst (Inf A) = (INF x\<in>A. fst x)" |
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
189 |
by (simp add: Inf_prod_def) |
44006 | 190 |
|
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
191 |
lemma fst_INF: "fst (INF x\<in>A. f x) = (INF x\<in>A. fst (f x))" |
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
192 |
by (simp add: fst_Inf image_image) |
44006 | 193 |
|
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
194 |
lemma fst_Sup: "fst (Sup A) = (SUP x\<in>A. fst x)" |
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
195 |
by (simp add: Sup_prod_def) |
44006 | 196 |
|
69260
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
67829
diff
changeset
|
197 |
lemma fst_SUP: "fst (SUP x\<in>A. f x) = (SUP x\<in>A. fst (f x))" |
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
198 |
by (simp add: fst_Sup image_image) |
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
199 |
|
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
200 |
lemma snd_Inf: "snd (Inf A) = (INF x\<in>A. snd x)" |
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
201 |
by (simp add: Inf_prod_def) |
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
202 |
|
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
203 |
lemma snd_INF: "snd (INF x\<in>A. f x) = (INF x\<in>A. snd (f x))" |
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
204 |
by (simp add: snd_Inf image_image) |
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
205 |
|
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
206 |
lemma snd_Sup: "snd (Sup A) = (SUP x\<in>A. snd x)" |
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
207 |
by (simp add: Sup_prod_def) |
44006 | 208 |
|
69260
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
67829
diff
changeset
|
209 |
lemma snd_SUP: "snd (SUP x\<in>A. f x) = (SUP x\<in>A. snd (f x))" |
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
210 |
by (simp add: snd_Sup image_image) |
44006 | 211 |
|
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
212 |
lemma INF_Pair: "(INF x\<in>A. (f x, g x)) = (INF x\<in>A. f x, INF x\<in>A. g x)" |
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
213 |
by (simp add: Inf_prod_def image_image) |
44006 | 214 |
|
69260
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
67829
diff
changeset
|
215 |
lemma SUP_Pair: "(SUP x\<in>A. (f x, g x)) = (SUP x\<in>A. f x, SUP x\<in>A. g x)" |
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
216 |
by (simp add: Sup_prod_def image_image) |
44006 | 217 |
|
50535 | 218 |
|
60500 | 219 |
text \<open>Alternative formulations for set infima and suprema over the product |
220 |
of two complete lattices:\<close> |
|
50535 | 221 |
|
69895
6b03a8cf092d
more formal contributors (with the help of the history);
wenzelm
parents:
69861
diff
changeset
|
222 |
lemma INF_prod_alt_def: \<^marker>\<open>contributor \<open>Alessandro Coglio\<close>\<close> |
69313 | 223 |
"Inf (f ` A) = (Inf ((fst \<circ> f) ` A), Inf ((snd \<circ> f) ` A))" |
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
224 |
by (simp add: Inf_prod_def image_image) |
50535 | 225 |
|
69895
6b03a8cf092d
more formal contributors (with the help of the history);
wenzelm
parents:
69861
diff
changeset
|
226 |
lemma SUP_prod_alt_def: \<^marker>\<open>contributor \<open>Alessandro Coglio\<close>\<close> |
69313 | 227 |
"Sup (f ` A) = (Sup ((fst \<circ> f) ` A), Sup((snd \<circ> f) ` A))" |
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
228 |
by (simp add: Sup_prod_def image_image) |
50535 | 229 |
|
230 |
||
60500 | 231 |
subsection \<open>Complete distributive lattices\<close> |
50535 | 232 |
|
69895
6b03a8cf092d
more formal contributors (with the help of the history);
wenzelm
parents:
69861
diff
changeset
|
233 |
instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice \<^marker>\<open>contributor \<open>Alessandro Coglio\<close>\<close> |
67829
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset
|
234 |
proof |
2a6ef5ba4822
Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents:
67091
diff
changeset
|
235 |
fix A::"('a\<times>'b) set set" |
69313 | 236 |
show "Inf (Sup ` A) \<le> Sup (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})" |
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69313
diff
changeset
|
237 |
by (simp add: Inf_prod_def Sup_prod_def INF_SUP_set image_image) |
50535 | 238 |
qed |
239 |
||
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
240 |
subsection \<open>Bekic's Theorem\<close> |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
241 |
text \<open> |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
242 |
Simultaneous fixed points over pairs can be written in terms of separate fixed points. |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
243 |
Transliterated from HOLCF.Fix by Peter Gammie |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
244 |
\<close> |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
245 |
|
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
246 |
lemma lfp_prod: |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
247 |
fixes F :: "'a::complete_lattice \<times> 'b::complete_lattice \<Rightarrow> 'a \<times> 'b" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
248 |
assumes "mono F" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
249 |
shows "lfp F = (lfp (\<lambda>x. fst (F (x, lfp (\<lambda>y. snd (F (x, y)))))), |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
250 |
(lfp (\<lambda>y. snd (F (lfp (\<lambda>x. fst (F (x, lfp (\<lambda>y. snd (F (x, y)))))), y)))))" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
251 |
(is "lfp F = (?x, ?y)") |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
252 |
proof(rule lfp_eqI[OF assms]) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
253 |
have 1: "fst (F (?x, ?y)) = ?x" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
254 |
by (rule trans [symmetric, OF lfp_unfold]) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
255 |
(blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono lfp_mono)+ |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
256 |
have 2: "snd (F (?x, ?y)) = ?y" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
257 |
by (rule trans [symmetric, OF lfp_unfold]) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
258 |
(blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono lfp_mono)+ |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
259 |
from 1 2 show "F (?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
260 |
next |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
261 |
fix z assume F_z: "F z = z" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
262 |
obtain x y where z: "z = (x, y)" by (rule prod.exhaust) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
263 |
from F_z z have F_x: "fst (F (x, y)) = x" by simp |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
264 |
from F_z z have F_y: "snd (F (x, y)) = y" by simp |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
265 |
let ?y1 = "lfp (\<lambda>y. snd (F (x, y)))" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
266 |
have "?y1 \<le> y" by (rule lfp_lowerbound, simp add: F_y) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
267 |
hence "fst (F (x, ?y1)) \<le> fst (F (x, y))" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
268 |
by (simp add: assms fst_mono monoD) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
269 |
hence "fst (F (x, ?y1)) \<le> x" using F_x by simp |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
270 |
hence 1: "?x \<le> x" by (simp add: lfp_lowerbound) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
271 |
hence "snd (F (?x, y)) \<le> snd (F (x, y))" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
272 |
by (simp add: assms snd_mono monoD) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
273 |
hence "snd (F (?x, y)) \<le> y" using F_y by simp |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
274 |
hence 2: "?y \<le> y" by (simp add: lfp_lowerbound) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
275 |
show "(?x, ?y) \<le> z" using z 1 2 by simp |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
276 |
qed |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
277 |
|
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
278 |
lemma gfp_prod: |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
279 |
fixes F :: "'a::complete_lattice \<times> 'b::complete_lattice \<Rightarrow> 'a \<times> 'b" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
280 |
assumes "mono F" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
281 |
shows "gfp F = (gfp (\<lambda>x. fst (F (x, gfp (\<lambda>y. snd (F (x, y)))))), |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
282 |
(gfp (\<lambda>y. snd (F (gfp (\<lambda>x. fst (F (x, gfp (\<lambda>y. snd (F (x, y)))))), y)))))" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
283 |
(is "gfp F = (?x, ?y)") |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
284 |
proof(rule gfp_eqI[OF assms]) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
285 |
have 1: "fst (F (?x, ?y)) = ?x" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
286 |
by (rule trans [symmetric, OF gfp_unfold]) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
287 |
(blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono gfp_mono)+ |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
288 |
have 2: "snd (F (?x, ?y)) = ?y" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
289 |
by (rule trans [symmetric, OF gfp_unfold]) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
290 |
(blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono gfp_mono)+ |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
291 |
from 1 2 show "F (?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
292 |
next |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
293 |
fix z assume F_z: "F z = z" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
294 |
obtain x y where z: "z = (x, y)" by (rule prod.exhaust) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
295 |
from F_z z have F_x: "fst (F (x, y)) = x" by simp |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
296 |
from F_z z have F_y: "snd (F (x, y)) = y" by simp |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
297 |
let ?y1 = "gfp (\<lambda>y. snd (F (x, y)))" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
298 |
have "y \<le> ?y1" by (rule gfp_upperbound, simp add: F_y) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
299 |
hence "fst (F (x, y)) \<le> fst (F (x, ?y1))" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
300 |
by (simp add: assms fst_mono monoD) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
301 |
hence "x \<le> fst (F (x, ?y1))" using F_x by simp |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
302 |
hence 1: "x \<le> ?x" by (simp add: gfp_upperbound) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
303 |
hence "snd (F (x, y)) \<le> snd (F (?x, y))" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
304 |
by (simp add: assms snd_mono monoD) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
305 |
hence "y \<le> snd (F (?x, y))" using F_y by simp |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
306 |
hence 2: "y \<le> ?y" by (simp add: gfp_upperbound) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
307 |
show "z \<le> (?x, ?y)" using z 1 2 by simp |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
308 |
qed |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
62343
diff
changeset
|
309 |
|
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
50573
diff
changeset
|
310 |
end |