new theory HOL/Library/Product_Lattice.thy
authorhuffman
Mon Aug 01 09:31:10 2011 -0700 (2011-08-01)
changeset 44006b9839fad3bb6
parent 44005 421f8bc19ce4
child 44009 9be0f4a6f155
new theory HOL/Library/Product_Lattice.thy
src/HOL/IsaMakefile
src/HOL/Library/Product_Lattice.thy
src/HOL/Library/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Sun Jul 31 11:13:38 2011 -0700
     1.2 +++ b/src/HOL/IsaMakefile	Mon Aug 01 09:31:10 2011 -0700
     1.3 @@ -470,6 +470,7 @@
     1.4    Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy	\
     1.5    Library/Preorder.thy Library/Product_Vector.thy			\
     1.6    Library/Product_ord.thy Library/Product_plus.thy			\
     1.7 +  Library/Product_Lattice.thy						\
     1.8    Library/Quickcheck_Types.thy						\
     1.9    Library/Quotient_List.thy Library/Quotient_Option.thy			\
    1.10    Library/Quotient_Product.thy Library/Quotient_Sum.thy			\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Product_Lattice.thy	Mon Aug 01 09:31:10 2011 -0700
     2.3 @@ -0,0 +1,198 @@
     2.4 +(*  Title:      Product_Lattice.thy
     2.5 +    Author:     Brian Huffman
     2.6 +*)
     2.7 +
     2.8 +header {* Lattice operations on product types *}
     2.9 +
    2.10 +theory Product_Lattice
    2.11 +imports "~~/src/HOL/Library/Product_plus"
    2.12 +begin
    2.13 +
    2.14 +subsection {* Pointwise ordering *}
    2.15 +
    2.16 +instantiation prod :: (ord, ord) ord
    2.17 +begin
    2.18 +
    2.19 +definition
    2.20 +  "x \<le> y \<longleftrightarrow> fst x \<le> fst y \<and> snd x \<le> snd y"
    2.21 +
    2.22 +definition
    2.23 +  "(x::'a \<times> 'b) < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
    2.24 +
    2.25 +instance ..
    2.26 +
    2.27 +end
    2.28 +
    2.29 +lemma fst_mono: "x \<le> y \<Longrightarrow> fst x \<le> fst y"
    2.30 +  unfolding less_eq_prod_def by simp
    2.31 +
    2.32 +lemma snd_mono: "x \<le> y \<Longrightarrow> snd x \<le> snd y"
    2.33 +  unfolding less_eq_prod_def by simp
    2.34 +
    2.35 +lemma Pair_mono: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> (x, y) \<le> (x', y')"
    2.36 +  unfolding less_eq_prod_def by simp
    2.37 +
    2.38 +lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d"
    2.39 +  unfolding less_eq_prod_def by simp
    2.40 +
    2.41 +instance prod :: (preorder, preorder) preorder
    2.42 +proof
    2.43 +  fix x y z :: "'a \<times> 'b"
    2.44 +  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
    2.45 +    by (rule less_prod_def)
    2.46 +  show "x \<le> x"
    2.47 +    unfolding less_eq_prod_def
    2.48 +    by fast
    2.49 +  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
    2.50 +    unfolding less_eq_prod_def
    2.51 +    by (fast elim: order_trans)
    2.52 +qed
    2.53 +
    2.54 +instance prod :: (order, order) order
    2.55 +  by default auto
    2.56 +
    2.57 +
    2.58 +subsection {* Binary infimum and supremum *}
    2.59 +
    2.60 +instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf
    2.61 +begin
    2.62 +
    2.63 +definition
    2.64 +  "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
    2.65 +
    2.66 +lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
    2.67 +  unfolding inf_prod_def by simp
    2.68 +
    2.69 +lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)"
    2.70 +  unfolding inf_prod_def by simp
    2.71 +
    2.72 +lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
    2.73 +  unfolding inf_prod_def by simp
    2.74 +
    2.75 +instance
    2.76 +  by default auto
    2.77 +
    2.78 +end
    2.79 +
    2.80 +instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup
    2.81 +begin
    2.82 +
    2.83 +definition
    2.84 +  "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))"
    2.85 +
    2.86 +lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)"
    2.87 +  unfolding sup_prod_def by simp
    2.88 +
    2.89 +lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)"
    2.90 +  unfolding sup_prod_def by simp
    2.91 +
    2.92 +lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
    2.93 +  unfolding sup_prod_def by simp
    2.94 +
    2.95 +instance
    2.96 +  by default auto
    2.97 +
    2.98 +end
    2.99 +
   2.100 +instance prod :: (lattice, lattice) lattice ..
   2.101 +
   2.102 +instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
   2.103 +  by default (auto simp add: sup_inf_distrib1)
   2.104 +
   2.105 +
   2.106 +subsection {* Top and bottom elements *}
   2.107 +
   2.108 +instantiation prod :: (top, top) top
   2.109 +begin
   2.110 +
   2.111 +definition
   2.112 +  "top = (top, top)"
   2.113 +
   2.114 +lemma fst_top [simp]: "fst top = top"
   2.115 +  unfolding top_prod_def by simp
   2.116 +
   2.117 +lemma snd_top [simp]: "snd top = top"
   2.118 +  unfolding top_prod_def by simp
   2.119 +
   2.120 +lemma Pair_top_top: "(top, top) = top"
   2.121 +  unfolding top_prod_def by simp
   2.122 +
   2.123 +instance
   2.124 +  by default (auto simp add: top_prod_def)
   2.125 +
   2.126 +end
   2.127 +
   2.128 +instantiation prod :: (bot, bot) bot
   2.129 +begin
   2.130 +
   2.131 +definition
   2.132 +  "bot = (bot, bot)"
   2.133 +
   2.134 +lemma fst_bot [simp]: "fst bot = bot"
   2.135 +  unfolding bot_prod_def by simp
   2.136 +
   2.137 +lemma snd_bot [simp]: "snd bot = bot"
   2.138 +  unfolding bot_prod_def by simp
   2.139 +
   2.140 +lemma Pair_bot_bot: "(bot, bot) = bot"
   2.141 +  unfolding bot_prod_def by simp
   2.142 +
   2.143 +instance
   2.144 +  by default (auto simp add: bot_prod_def)
   2.145 +
   2.146 +end
   2.147 +
   2.148 +instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
   2.149 +
   2.150 +instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
   2.151 +  by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
   2.152 +
   2.153 +
   2.154 +subsection {* Complete lattice operations *}
   2.155 +
   2.156 +instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
   2.157 +begin
   2.158 +
   2.159 +definition
   2.160 +  "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
   2.161 +
   2.162 +definition
   2.163 +  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
   2.164 +
   2.165 +instance
   2.166 +  by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
   2.167 +    INF_leI le_SUPI le_INF_iff SUP_le_iff)
   2.168 +
   2.169 +end
   2.170 +
   2.171 +lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
   2.172 +  unfolding Sup_prod_def by simp
   2.173 +
   2.174 +lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
   2.175 +  unfolding Sup_prod_def by simp
   2.176 +
   2.177 +lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
   2.178 +  unfolding Inf_prod_def by simp
   2.179 +
   2.180 +lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
   2.181 +  unfolding Inf_prod_def by simp
   2.182 +
   2.183 +lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
   2.184 +  by (simp add: SUPR_def fst_Sup image_image)
   2.185 +
   2.186 +lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
   2.187 +  by (simp add: SUPR_def snd_Sup image_image)
   2.188 +
   2.189 +lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
   2.190 +  by (simp add: INFI_def fst_Inf image_image)
   2.191 +
   2.192 +lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
   2.193 +  by (simp add: INFI_def snd_Inf image_image)
   2.194 +
   2.195 +lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
   2.196 +  by (simp add: SUPR_def Sup_prod_def image_image)
   2.197 +
   2.198 +lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
   2.199 +  by (simp add: INFI_def Inf_prod_def image_image)
   2.200 +
   2.201 +end
     3.1 --- a/src/HOL/Library/ROOT.ML	Sun Jul 31 11:13:38 2011 -0700
     3.2 +++ b/src/HOL/Library/ROOT.ML	Mon Aug 01 09:31:10 2011 -0700
     3.3 @@ -2,4 +2,5 @@
     3.4  (* Classical Higher-order Logic -- batteries included *)
     3.5  
     3.6  use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
     3.7 +  "Product_Lattice",
     3.8    "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];