# Theory Product_Lattice

Up to index of Isabelle/HOL/HOL-Library

theory Product_Lattice
imports Product_plus
`(*  Title:      HOL/Library/Product_Lattice.thy    Author:     Brian Huffman*)header {* Lattice operations on product types *}theory Product_Latticeimports "~~/src/HOL/Library/Product_plus"beginsubsection {* Pointwise ordering *}instantiation prod :: (ord, ord) ordbegindefinition  "x ≤ y <-> fst x ≤ fst y ∧ snd x ≤ snd y"definition  "(x::'a × 'b) < y <-> x ≤ y ∧ ¬ y ≤ x"instance ..endlemma fst_mono: "x ≤ y ==> fst x ≤ fst y"  unfolding less_eq_prod_def by simplemma snd_mono: "x ≤ y ==> snd x ≤ snd y"  unfolding less_eq_prod_def by simplemma Pair_mono: "x ≤ x' ==> y ≤ y' ==> (x, y) ≤ (x', y')"  unfolding less_eq_prod_def by simplemma Pair_le [simp]: "(a, b) ≤ (c, d) <-> a ≤ c ∧ b ≤ d"  unfolding less_eq_prod_def by simpinstance prod :: (preorder, preorder) preorderproof  fix x y z :: "'a × 'b"  show "x < y <-> x ≤ y ∧ ¬ y ≤ x"    by (rule less_prod_def)  show "x ≤ x"    unfolding less_eq_prod_def    by fast  assume "x ≤ y" and "y ≤ z" thus "x ≤ z"    unfolding less_eq_prod_def    by (fast elim: order_trans)qedinstance prod :: (order, order) order  by default autosubsection {* Binary infimum and supremum *}instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_infbegindefinition  "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"  unfolding inf_prod_def by simplemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)"  unfolding inf_prod_def by simplemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"  unfolding inf_prod_def by simpinstance  by default autoendinstantiation prod :: (semilattice_sup, semilattice_sup) semilattice_supbegindefinition  "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))"lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)"  unfolding sup_prod_def by simplemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)"  unfolding sup_prod_def by simplemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"  unfolding sup_prod_def by simpinstance  by default autoendinstance prod :: (lattice, lattice) lattice ..instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice  by default (auto simp add: sup_inf_distrib1)subsection {* Top and bottom elements *}instantiation prod :: (top, top) topbegindefinition  "top = (top, top)"lemma fst_top [simp]: "fst top = top"  unfolding top_prod_def by simplemma snd_top [simp]: "snd top = top"  unfolding top_prod_def by simplemma Pair_top_top: "(top, top) = top"  unfolding top_prod_def by simpinstance  by default (auto simp add: top_prod_def)endinstantiation prod :: (bot, bot) botbegindefinition  "bot = (bot, bot)"lemma fst_bot [simp]: "fst bot = bot"  unfolding bot_prod_def by simplemma snd_bot [simp]: "snd bot = bot"  unfolding bot_prod_def by simplemma Pair_bot_bot: "(bot, bot) = bot"  unfolding bot_prod_def by simpinstance  by default (auto simp add: bot_prod_def)endinstance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra  by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)subsection {* Complete lattice operations *}instantiation prod :: (complete_lattice, complete_lattice) complete_latticebegindefinition  "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"definition  "Inf A = (INF x:A. fst x, INF x:A. snd x)"instance  by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def    INF_lower SUP_upper le_INF_iff SUP_le_iff)endlemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"  unfolding Sup_prod_def by simplemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"  unfolding Sup_prod_def by simplemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"  unfolding Inf_prod_def by simplemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"  unfolding Inf_prod_def by simplemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"  by (simp add: SUP_def fst_Sup image_image)lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"  by (simp add: SUP_def snd_Sup image_image)lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"  by (simp add: INF_def fst_Inf image_image)lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"  by (simp add: INF_def snd_Inf image_image)lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"  by (simp add: SUP_def Sup_prod_def image_image)lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"  by (simp add: INF_def Inf_prod_def image_image)text {* Alternative formulations for set infima and suprema over the productof two complete lattices: *}lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"by (auto simp: Inf_prod_def INF_def)lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"by (auto simp: Sup_prod_def SUP_def)lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"by (auto simp: INF_def Inf_prod_def image_compose)lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"by (auto simp: SUP_def Sup_prod_def image_compose)lemma INF_prod_alt_def:  "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"by (metis fst_INF snd_INF surjective_pairing)lemma SUP_prod_alt_def:  "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"by (metis fst_SUP snd_SUP surjective_pairing)subsection {* Complete distributive lattices *}(* Contribution: Alessandro Coglio *)instance prod ::  (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_latticeproof  case goal1 thus ?case    by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF)next  case goal2 thus ?case    by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP)qedend`