src/HOL/Library/Product_Order.thy
changeset 51115 7dbd6832a689
parent 50573 765c22baa1c9
child 51542 738598beeb26
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Product_Order.thy	Thu Feb 14 14:14:55 2013 +0100
     1.3 @@ -0,0 +1,238 @@
     1.4 +(*  Title:      HOL/Library/Product_Order.thy
     1.5 +    Author:     Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +header {* Pointwise order on product types *}
     1.9 +
    1.10 +theory Product_Order
    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_lower SUP_upper 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: SUP_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: SUP_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: INF_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: INF_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: SUP_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: INF_def Inf_prod_def image_image)
   1.200 +
   1.201 +
   1.202 +text {* Alternative formulations for set infima and suprema over the product
   1.203 +of two complete lattices: *}
   1.204 +
   1.205 +lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
   1.206 +by (auto simp: Inf_prod_def INF_def)
   1.207 +
   1.208 +lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
   1.209 +by (auto simp: Sup_prod_def SUP_def)
   1.210 +
   1.211 +lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
   1.212 +by (auto simp: INF_def Inf_prod_def image_compose)
   1.213 +
   1.214 +lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
   1.215 +by (auto simp: SUP_def Sup_prod_def image_compose)
   1.216 +
   1.217 +lemma INF_prod_alt_def:
   1.218 +  "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
   1.219 +by (metis fst_INF snd_INF surjective_pairing)
   1.220 +
   1.221 +lemma SUP_prod_alt_def:
   1.222 +  "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
   1.223 +by (metis fst_SUP snd_SUP surjective_pairing)
   1.224 +
   1.225 +
   1.226 +subsection {* Complete distributive lattices *}
   1.227 +
   1.228 +(* Contribution: Alessandro Coglio *)
   1.229 +
   1.230 +instance prod ::
   1.231 +  (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
   1.232 +proof
   1.233 +  case goal1 thus ?case
   1.234 +    by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF)
   1.235 +next
   1.236 +  case goal2 thus ?case
   1.237 +    by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP)
   1.238 +qed
   1.239 +
   1.240 +end
   1.241 +