wenzelm@45007: (* Title: HOL/Library/Product_Lattice.thy huffman@44006: Author: Brian Huffman huffman@44006: *) huffman@44006: huffman@44006: header {* Lattice operations on product types *} huffman@44006: huffman@44006: theory Product_Lattice huffman@44006: imports "~~/src/HOL/Library/Product_plus" huffman@44006: begin huffman@44006: huffman@44006: subsection {* Pointwise ordering *} huffman@44006: huffman@44006: instantiation prod :: (ord, ord) ord huffman@44006: begin huffman@44006: huffman@44006: definition huffman@44006: "x \ y \ fst x \ fst y \ snd x \ snd y" huffman@44006: huffman@44006: definition huffman@44006: "(x::'a \ 'b) < y \ x \ y \ \ y \ x" huffman@44006: huffman@44006: instance .. huffman@44006: huffman@44006: end huffman@44006: huffman@44006: lemma fst_mono: "x \ y \ fst x \ fst y" huffman@44006: unfolding less_eq_prod_def by simp huffman@44006: huffman@44006: lemma snd_mono: "x \ y \ snd x \ snd y" huffman@44006: unfolding less_eq_prod_def by simp huffman@44006: huffman@44006: lemma Pair_mono: "x \ x' \ y \ y' \ (x, y) \ (x', y')" huffman@44006: unfolding less_eq_prod_def by simp huffman@44006: huffman@44006: lemma Pair_le [simp]: "(a, b) \ (c, d) \ a \ c \ b \ d" huffman@44006: unfolding less_eq_prod_def by simp huffman@44006: huffman@44006: instance prod :: (preorder, preorder) preorder huffman@44006: proof huffman@44006: fix x y z :: "'a \ 'b" huffman@44006: show "x < y \ x \ y \ \ y \ x" huffman@44006: by (rule less_prod_def) huffman@44006: show "x \ x" huffman@44006: unfolding less_eq_prod_def huffman@44006: by fast huffman@44006: assume "x \ y" and "y \ z" thus "x \ z" huffman@44006: unfolding less_eq_prod_def huffman@44006: by (fast elim: order_trans) huffman@44006: qed huffman@44006: huffman@44006: instance prod :: (order, order) order huffman@44006: by default auto huffman@44006: huffman@44006: huffman@44006: subsection {* Binary infimum and supremum *} huffman@44006: huffman@44006: instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf huffman@44006: begin huffman@44006: huffman@44006: definition huffman@44006: "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))" huffman@44006: huffman@44006: lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)" huffman@44006: unfolding inf_prod_def by simp huffman@44006: huffman@44006: lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)" huffman@44006: unfolding inf_prod_def by simp huffman@44006: huffman@44006: lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)" huffman@44006: unfolding inf_prod_def by simp huffman@44006: huffman@44006: instance huffman@44006: by default auto huffman@44006: huffman@44006: end huffman@44006: huffman@44006: instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup huffman@44006: begin huffman@44006: huffman@44006: definition huffman@44006: "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))" huffman@44006: huffman@44006: lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)" huffman@44006: unfolding sup_prod_def by simp huffman@44006: huffman@44006: lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)" huffman@44006: unfolding sup_prod_def by simp huffman@44006: huffman@44006: lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)" huffman@44006: unfolding sup_prod_def by simp huffman@44006: huffman@44006: instance huffman@44006: by default auto huffman@44006: huffman@44006: end huffman@44006: huffman@44006: instance prod :: (lattice, lattice) lattice .. huffman@44006: huffman@44006: instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice huffman@44006: by default (auto simp add: sup_inf_distrib1) huffman@44006: huffman@44006: huffman@44006: subsection {* Top and bottom elements *} huffman@44006: huffman@44006: instantiation prod :: (top, top) top huffman@44006: begin huffman@44006: huffman@44006: definition huffman@44006: "top = (top, top)" huffman@44006: huffman@44006: lemma fst_top [simp]: "fst top = top" huffman@44006: unfolding top_prod_def by simp huffman@44006: huffman@44006: lemma snd_top [simp]: "snd top = top" huffman@44006: unfolding top_prod_def by simp huffman@44006: huffman@44006: lemma Pair_top_top: "(top, top) = top" huffman@44006: unfolding top_prod_def by simp huffman@44006: huffman@44006: instance huffman@44006: by default (auto simp add: top_prod_def) huffman@44006: huffman@44006: end huffman@44006: huffman@44006: instantiation prod :: (bot, bot) bot huffman@44006: begin huffman@44006: huffman@44006: definition huffman@44006: "bot = (bot, bot)" huffman@44006: huffman@44006: lemma fst_bot [simp]: "fst bot = bot" huffman@44006: unfolding bot_prod_def by simp huffman@44006: huffman@44006: lemma snd_bot [simp]: "snd bot = bot" huffman@44006: unfolding bot_prod_def by simp huffman@44006: huffman@44006: lemma Pair_bot_bot: "(bot, bot) = bot" huffman@44006: unfolding bot_prod_def by simp huffman@44006: huffman@44006: instance huffman@44006: by default (auto simp add: bot_prod_def) huffman@44006: huffman@44006: end huffman@44006: huffman@44006: instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice .. huffman@44006: huffman@44006: instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra huffman@44006: by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq) huffman@44006: huffman@44006: huffman@44006: subsection {* Complete lattice operations *} huffman@44006: huffman@44006: instantiation prod :: (complete_lattice, complete_lattice) complete_lattice huffman@44006: begin huffman@44006: huffman@44006: definition huffman@44006: "Sup A = (SUP x:A. fst x, SUP x:A. snd x)" huffman@44006: huffman@44006: definition huffman@44006: "Inf A = (INF x:A. fst x, INF x:A. snd x)" huffman@44006: huffman@44006: instance huffman@44006: by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def hoelzl@44928: INF_lower SUP_upper le_INF_iff SUP_le_iff) huffman@44006: huffman@44006: end huffman@44006: huffman@44006: lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)" huffman@44006: unfolding Sup_prod_def by simp huffman@44006: huffman@44006: lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)" huffman@44006: unfolding Sup_prod_def by simp huffman@44006: huffman@44006: lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)" huffman@44006: unfolding Inf_prod_def by simp huffman@44006: huffman@44006: lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)" huffman@44006: unfolding Inf_prod_def by simp huffman@44006: huffman@44006: lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))" hoelzl@44928: by (simp add: SUP_def fst_Sup image_image) huffman@44006: huffman@44006: lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))" hoelzl@44928: by (simp add: SUP_def snd_Sup image_image) huffman@44006: huffman@44006: lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))" hoelzl@44928: by (simp add: INF_def fst_Inf image_image) huffman@44006: huffman@44006: lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))" hoelzl@44928: by (simp add: INF_def snd_Inf image_image) huffman@44006: huffman@44006: lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)" hoelzl@44928: by (simp add: SUP_def Sup_prod_def image_image) huffman@44006: huffman@44006: lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)" hoelzl@44928: by (simp add: INF_def Inf_prod_def image_image) huffman@44006: huffman@44006: end