1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Library/Product_Lattice.thy Mon Aug 01 09:31:10 2011 -0700
1.3 @@ -0,0 +1,198 @@
1.4 +(* Title: Product_Lattice.thy
1.5 + Author: Brian Huffman
1.6 +*)
1.7 +
1.8 +header {* Lattice operations on product types *}
1.9 +
1.10 +theory Product_Lattice
1.11 +imports "~~/src/HOL/Library/Product_plus"
1.12 +begin
1.13 +
1.14 +subsection {* Pointwise ordering *}
1.15 +
1.16 +instantiation prod :: (ord, ord) ord
1.17 +begin
1.18 +
1.19 +definition
1.20 + "x \<le> y \<longleftrightarrow> fst x \<le> fst y \<and> snd x \<le> snd y"
1.21 +
1.22 +definition
1.23 + "(x::'a \<times> 'b) < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
1.24 +
1.25 +instance ..
1.26 +
1.27 +end
1.28 +
1.29 +lemma fst_mono: "x \<le> y \<Longrightarrow> fst x \<le> fst y"
1.30 + unfolding less_eq_prod_def by simp
1.31 +
1.32 +lemma snd_mono: "x \<le> y \<Longrightarrow> snd x \<le> snd y"
1.33 + unfolding less_eq_prod_def by simp
1.34 +
1.35 +lemma Pair_mono: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> (x, y) \<le> (x', y')"
1.36 + unfolding less_eq_prod_def by simp
1.37 +
1.38 +lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d"
1.39 + unfolding less_eq_prod_def by simp
1.40 +
1.41 +instance prod :: (preorder, preorder) preorder
1.42 +proof
1.43 + fix x y z :: "'a \<times> 'b"
1.44 + show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
1.45 + by (rule less_prod_def)
1.46 + show "x \<le> x"
1.47 + unfolding less_eq_prod_def
1.48 + by fast
1.49 + assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
1.50 + unfolding less_eq_prod_def
1.51 + by (fast elim: order_trans)
1.52 +qed
1.53 +
1.54 +instance prod :: (order, order) order
1.55 + by default auto
1.56 +
1.57 +
1.58 +subsection {* Binary infimum and supremum *}
1.59 +
1.60 +instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf
1.61 +begin
1.62 +
1.63 +definition
1.64 + "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
1.65 +
1.66 +lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
1.67 + unfolding inf_prod_def by simp
1.68 +
1.69 +lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)"
1.70 + unfolding inf_prod_def by simp
1.71 +
1.72 +lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
1.73 + unfolding inf_prod_def by simp
1.74 +
1.75 +instance
1.76 + by default auto
1.77 +
1.78 +end
1.79 +
1.80 +instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup
1.81 +begin
1.82 +
1.83 +definition
1.84 + "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))"
1.85 +
1.86 +lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)"
1.87 + unfolding sup_prod_def by simp
1.88 +
1.89 +lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)"
1.90 + unfolding sup_prod_def by simp
1.91 +
1.92 +lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
1.93 + unfolding sup_prod_def by simp
1.94 +
1.95 +instance
1.96 + by default auto
1.97 +
1.98 +end
1.99 +
1.100 +instance prod :: (lattice, lattice) lattice ..
1.101 +
1.102 +instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
1.103 + by default (auto simp add: sup_inf_distrib1)
1.104 +
1.105 +
1.106 +subsection {* Top and bottom elements *}
1.107 +
1.108 +instantiation prod :: (top, top) top
1.109 +begin
1.110 +
1.111 +definition
1.112 + "top = (top, top)"
1.113 +
1.114 +lemma fst_top [simp]: "fst top = top"
1.115 + unfolding top_prod_def by simp
1.116 +
1.117 +lemma snd_top [simp]: "snd top = top"
1.118 + unfolding top_prod_def by simp
1.119 +
1.120 +lemma Pair_top_top: "(top, top) = top"
1.121 + unfolding top_prod_def by simp
1.122 +
1.123 +instance
1.124 + by default (auto simp add: top_prod_def)
1.125 +
1.126 +end
1.127 +
1.128 +instantiation prod :: (bot, bot) bot
1.129 +begin
1.130 +
1.131 +definition
1.132 + "bot = (bot, bot)"
1.133 +
1.134 +lemma fst_bot [simp]: "fst bot = bot"
1.135 + unfolding bot_prod_def by simp
1.136 +
1.137 +lemma snd_bot [simp]: "snd bot = bot"
1.138 + unfolding bot_prod_def by simp
1.139 +
1.140 +lemma Pair_bot_bot: "(bot, bot) = bot"
1.141 + unfolding bot_prod_def by simp
1.142 +
1.143 +instance
1.144 + by default (auto simp add: bot_prod_def)
1.145 +
1.146 +end
1.147 +
1.148 +instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
1.149 +
1.150 +instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
1.151 + by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
1.152 +
1.153 +
1.154 +subsection {* Complete lattice operations *}
1.155 +
1.156 +instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
1.157 +begin
1.158 +
1.159 +definition
1.160 + "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
1.161 +
1.162 +definition
1.163 + "Inf A = (INF x:A. fst x, INF x:A. snd x)"
1.164 +
1.165 +instance
1.166 + by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
1.167 + INF_leI le_SUPI le_INF_iff SUP_le_iff)
1.168 +
1.169 +end
1.170 +
1.171 +lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
1.172 + unfolding Sup_prod_def by simp
1.173 +
1.174 +lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
1.175 + unfolding Sup_prod_def by simp
1.176 +
1.177 +lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
1.178 + unfolding Inf_prod_def by simp
1.179 +
1.180 +lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
1.181 + unfolding Inf_prod_def by simp
1.182 +
1.183 +lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
1.184 + by (simp add: SUPR_def fst_Sup image_image)
1.185 +
1.186 +lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
1.187 + by (simp add: SUPR_def snd_Sup image_image)
1.188 +
1.189 +lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
1.190 + by (simp add: INFI_def fst_Inf image_image)
1.191 +
1.192 +lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
1.193 + by (simp add: INFI_def snd_Inf image_image)
1.194 +
1.195 +lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
1.196 + by (simp add: SUPR_def Sup_prod_def image_image)
1.197 +
1.198 +lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
1.199 + by (simp add: INFI_def Inf_prod_def image_image)
1.200 +
1.201 +end