44006
|
1 |
(* Title: Product_Lattice.thy
|
|
2 |
Author: Brian Huffman
|
|
3 |
*)
|
|
4 |
|
|
5 |
header {* Lattice operations on product types *}
|
|
6 |
|
|
7 |
theory Product_Lattice
|
|
8 |
imports "~~/src/HOL/Library/Product_plus"
|
|
9 |
begin
|
|
10 |
|
|
11 |
subsection {* Pointwise ordering *}
|
|
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
|
|
52 |
by default auto
|
|
53 |
|
|
54 |
|
|
55 |
subsection {* Binary infimum and supremum *}
|
|
56 |
|
|
57 |
instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf
|
|
58 |
begin
|
|
59 |
|
|
60 |
definition
|
|
61 |
"inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
|
|
62 |
|
|
63 |
lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
|
|
64 |
unfolding inf_prod_def by simp
|
|
65 |
|
|
66 |
lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)"
|
|
67 |
unfolding inf_prod_def by simp
|
|
68 |
|
|
69 |
lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
|
|
70 |
unfolding inf_prod_def by simp
|
|
71 |
|
|
72 |
instance
|
|
73 |
by default auto
|
|
74 |
|
|
75 |
end
|
|
76 |
|
|
77 |
instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup
|
|
78 |
begin
|
|
79 |
|
|
80 |
definition
|
|
81 |
"sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))"
|
|
82 |
|
|
83 |
lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)"
|
|
84 |
unfolding sup_prod_def by simp
|
|
85 |
|
|
86 |
lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)"
|
|
87 |
unfolding sup_prod_def by simp
|
|
88 |
|
|
89 |
lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
|
|
90 |
unfolding sup_prod_def by simp
|
|
91 |
|
|
92 |
instance
|
|
93 |
by default auto
|
|
94 |
|
|
95 |
end
|
|
96 |
|
|
97 |
instance prod :: (lattice, lattice) lattice ..
|
|
98 |
|
|
99 |
instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
|
|
100 |
by default (auto simp add: sup_inf_distrib1)
|
|
101 |
|
|
102 |
|
|
103 |
subsection {* Top and bottom elements *}
|
|
104 |
|
|
105 |
instantiation prod :: (top, top) top
|
|
106 |
begin
|
|
107 |
|
|
108 |
definition
|
|
109 |
"top = (top, top)"
|
|
110 |
|
|
111 |
lemma fst_top [simp]: "fst top = top"
|
|
112 |
unfolding top_prod_def by simp
|
|
113 |
|
|
114 |
lemma snd_top [simp]: "snd top = top"
|
|
115 |
unfolding top_prod_def by simp
|
|
116 |
|
|
117 |
lemma Pair_top_top: "(top, top) = top"
|
|
118 |
unfolding top_prod_def by simp
|
|
119 |
|
|
120 |
instance
|
|
121 |
by default (auto simp add: top_prod_def)
|
|
122 |
|
|
123 |
end
|
|
124 |
|
|
125 |
instantiation prod :: (bot, bot) bot
|
|
126 |
begin
|
|
127 |
|
|
128 |
definition
|
|
129 |
"bot = (bot, bot)"
|
|
130 |
|
|
131 |
lemma fst_bot [simp]: "fst bot = bot"
|
|
132 |
unfolding bot_prod_def by simp
|
|
133 |
|
|
134 |
lemma snd_bot [simp]: "snd bot = bot"
|
|
135 |
unfolding bot_prod_def by simp
|
|
136 |
|
|
137 |
lemma Pair_bot_bot: "(bot, bot) = bot"
|
|
138 |
unfolding bot_prod_def by simp
|
|
139 |
|
|
140 |
instance
|
|
141 |
by default (auto simp add: bot_prod_def)
|
|
142 |
|
|
143 |
end
|
|
144 |
|
|
145 |
instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
|
|
146 |
|
|
147 |
instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
|
|
148 |
by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
|
|
149 |
|
|
150 |
|
|
151 |
subsection {* Complete lattice operations *}
|
|
152 |
|
|
153 |
instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
|
|
154 |
begin
|
|
155 |
|
|
156 |
definition
|
|
157 |
"Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
|
|
158 |
|
|
159 |
definition
|
|
160 |
"Inf A = (INF x:A. fst x, INF x:A. snd x)"
|
|
161 |
|
|
162 |
instance
|
|
163 |
by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
|
|
164 |
INF_leI le_SUPI le_INF_iff SUP_le_iff)
|
|
165 |
|
|
166 |
end
|
|
167 |
|
|
168 |
lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
|
|
169 |
unfolding Sup_prod_def by simp
|
|
170 |
|
|
171 |
lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
|
|
172 |
unfolding Sup_prod_def by simp
|
|
173 |
|
|
174 |
lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
|
|
175 |
unfolding Inf_prod_def by simp
|
|
176 |
|
|
177 |
lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
|
|
178 |
unfolding Inf_prod_def by simp
|
|
179 |
|
|
180 |
lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
|
|
181 |
by (simp add: SUPR_def fst_Sup image_image)
|
|
182 |
|
|
183 |
lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
|
|
184 |
by (simp add: SUPR_def snd_Sup image_image)
|
|
185 |
|
|
186 |
lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
|
|
187 |
by (simp add: INFI_def fst_Inf image_image)
|
|
188 |
|
|
189 |
lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
|
|
190 |
by (simp add: INFI_def snd_Inf image_image)
|
|
191 |
|
|
192 |
lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
|
|
193 |
by (simp add: SUPR_def Sup_prod_def image_image)
|
|
194 |
|
|
195 |
lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
|
|
196 |
by (simp add: INFI_def Inf_prod_def image_image)
|
|
197 |
|
|
198 |
end
|