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
