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"*)];