merged
authorAndreas Lochbihler
Thu Feb 14 16:01:59 2013 +0100 (2013-02-14)
changeset 5111747af65ef228e
parent 51116 0dac0158b8d4
parent 51115 7dbd6832a689
child 51123 e51e76ffaedd
child 51124 8fd094d5b7b7
merged
src/HOL/Library/Product_Lattice.thy
src/HOL/Library/Product_ord.thy
     1.1 --- a/NEWS	Thu Feb 14 16:01:28 2013 +0100
     1.2 +++ b/NEWS	Thu Feb 14 16:01:59 2013 +0100
     1.3 @@ -10,6 +10,15 @@
     1.4  (lin)order_topology. Allows to generalize theorems about limits and
     1.5  order. Instances are reals and extended reals.
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Consolidation of library theories on product orders:
    1.10 +
    1.11 +    Product_Lattice ~> Product_Order -- pointwise order on products
    1.12 +    Product_ord ~> Product_Lexorder -- lexicographic order on products
    1.13 +
    1.14 +INCOMPATIBILITY.
    1.15 +
    1.16  
    1.17  New in Isabelle2013 (February 2013)
    1.18  -----------------------------------
     2.1 --- a/src/HOL/Library/Finite_Lattice.thy	Thu Feb 14 16:01:28 2013 +0100
     2.2 +++ b/src/HOL/Library/Finite_Lattice.thy	Thu Feb 14 16:01:59 2013 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  (* Author: Alessandro Coglio *)
     2.5  
     2.6  theory Finite_Lattice
     2.7 -imports Product_Lattice
     2.8 +imports Product_Order
     2.9  begin
    2.10  
    2.11  text {* A non-empty finite lattice is a complete lattice.
     3.1 --- a/src/HOL/Library/Product_Lattice.thy	Thu Feb 14 16:01:28 2013 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,238 +0,0 @@
     3.4 -(*  Title:      HOL/Library/Product_Lattice.thy
     3.5 -    Author:     Brian Huffman
     3.6 -*)
     3.7 -
     3.8 -header {* Lattice operations on product types *}
     3.9 -
    3.10 -theory Product_Lattice
    3.11 -imports "~~/src/HOL/Library/Product_plus"
    3.12 -begin
    3.13 -
    3.14 -subsection {* Pointwise ordering *}
    3.15 -
    3.16 -instantiation prod :: (ord, ord) ord
    3.17 -begin
    3.18 -
    3.19 -definition
    3.20 -  "x \<le> y \<longleftrightarrow> fst x \<le> fst y \<and> snd x \<le> snd y"
    3.21 -
    3.22 -definition
    3.23 -  "(x::'a \<times> 'b) < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
    3.24 -
    3.25 -instance ..
    3.26 -
    3.27 -end
    3.28 -
    3.29 -lemma fst_mono: "x \<le> y \<Longrightarrow> fst x \<le> fst y"
    3.30 -  unfolding less_eq_prod_def by simp
    3.31 -
    3.32 -lemma snd_mono: "x \<le> y \<Longrightarrow> snd x \<le> snd y"
    3.33 -  unfolding less_eq_prod_def by simp
    3.34 -
    3.35 -lemma Pair_mono: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> (x, y) \<le> (x', y')"
    3.36 -  unfolding less_eq_prod_def by simp
    3.37 -
    3.38 -lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d"
    3.39 -  unfolding less_eq_prod_def by simp
    3.40 -
    3.41 -instance prod :: (preorder, preorder) preorder
    3.42 -proof
    3.43 -  fix x y z :: "'a \<times> 'b"
    3.44 -  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
    3.45 -    by (rule less_prod_def)
    3.46 -  show "x \<le> x"
    3.47 -    unfolding less_eq_prod_def
    3.48 -    by fast
    3.49 -  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
    3.50 -    unfolding less_eq_prod_def
    3.51 -    by (fast elim: order_trans)
    3.52 -qed
    3.53 -
    3.54 -instance prod :: (order, order) order
    3.55 -  by default auto
    3.56 -
    3.57 -
    3.58 -subsection {* Binary infimum and supremum *}
    3.59 -
    3.60 -instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf
    3.61 -begin
    3.62 -
    3.63 -definition
    3.64 -  "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
    3.65 -
    3.66 -lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
    3.67 -  unfolding inf_prod_def by simp
    3.68 -
    3.69 -lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)"
    3.70 -  unfolding inf_prod_def by simp
    3.71 -
    3.72 -lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
    3.73 -  unfolding inf_prod_def by simp
    3.74 -
    3.75 -instance
    3.76 -  by default auto
    3.77 -
    3.78 -end
    3.79 -
    3.80 -instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup
    3.81 -begin
    3.82 -
    3.83 -definition
    3.84 -  "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))"
    3.85 -
    3.86 -lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)"
    3.87 -  unfolding sup_prod_def by simp
    3.88 -
    3.89 -lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)"
    3.90 -  unfolding sup_prod_def by simp
    3.91 -
    3.92 -lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
    3.93 -  unfolding sup_prod_def by simp
    3.94 -
    3.95 -instance
    3.96 -  by default auto
    3.97 -
    3.98 -end
    3.99 -
   3.100 -instance prod :: (lattice, lattice) lattice ..
   3.101 -
   3.102 -instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
   3.103 -  by default (auto simp add: sup_inf_distrib1)
   3.104 -
   3.105 -
   3.106 -subsection {* Top and bottom elements *}
   3.107 -
   3.108 -instantiation prod :: (top, top) top
   3.109 -begin
   3.110 -
   3.111 -definition
   3.112 -  "top = (top, top)"
   3.113 -
   3.114 -lemma fst_top [simp]: "fst top = top"
   3.115 -  unfolding top_prod_def by simp
   3.116 -
   3.117 -lemma snd_top [simp]: "snd top = top"
   3.118 -  unfolding top_prod_def by simp
   3.119 -
   3.120 -lemma Pair_top_top: "(top, top) = top"
   3.121 -  unfolding top_prod_def by simp
   3.122 -
   3.123 -instance
   3.124 -  by default (auto simp add: top_prod_def)
   3.125 -
   3.126 -end
   3.127 -
   3.128 -instantiation prod :: (bot, bot) bot
   3.129 -begin
   3.130 -
   3.131 -definition
   3.132 -  "bot = (bot, bot)"
   3.133 -
   3.134 -lemma fst_bot [simp]: "fst bot = bot"
   3.135 -  unfolding bot_prod_def by simp
   3.136 -
   3.137 -lemma snd_bot [simp]: "snd bot = bot"
   3.138 -  unfolding bot_prod_def by simp
   3.139 -
   3.140 -lemma Pair_bot_bot: "(bot, bot) = bot"
   3.141 -  unfolding bot_prod_def by simp
   3.142 -
   3.143 -instance
   3.144 -  by default (auto simp add: bot_prod_def)
   3.145 -
   3.146 -end
   3.147 -
   3.148 -instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
   3.149 -
   3.150 -instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
   3.151 -  by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
   3.152 -
   3.153 -
   3.154 -subsection {* Complete lattice operations *}
   3.155 -
   3.156 -instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
   3.157 -begin
   3.158 -
   3.159 -definition
   3.160 -  "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
   3.161 -
   3.162 -definition
   3.163 -  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
   3.164 -
   3.165 -instance
   3.166 -  by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
   3.167 -    INF_lower SUP_upper le_INF_iff SUP_le_iff)
   3.168 -
   3.169 -end
   3.170 -
   3.171 -lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
   3.172 -  unfolding Sup_prod_def by simp
   3.173 -
   3.174 -lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
   3.175 -  unfolding Sup_prod_def by simp
   3.176 -
   3.177 -lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
   3.178 -  unfolding Inf_prod_def by simp
   3.179 -
   3.180 -lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
   3.181 -  unfolding Inf_prod_def by simp
   3.182 -
   3.183 -lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
   3.184 -  by (simp add: SUP_def fst_Sup image_image)
   3.185 -
   3.186 -lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
   3.187 -  by (simp add: SUP_def snd_Sup image_image)
   3.188 -
   3.189 -lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
   3.190 -  by (simp add: INF_def fst_Inf image_image)
   3.191 -
   3.192 -lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
   3.193 -  by (simp add: INF_def snd_Inf image_image)
   3.194 -
   3.195 -lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
   3.196 -  by (simp add: SUP_def Sup_prod_def image_image)
   3.197 -
   3.198 -lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
   3.199 -  by (simp add: INF_def Inf_prod_def image_image)
   3.200 -
   3.201 -
   3.202 -text {* Alternative formulations for set infima and suprema over the product
   3.203 -of two complete lattices: *}
   3.204 -
   3.205 -lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
   3.206 -by (auto simp: Inf_prod_def INF_def)
   3.207 -
   3.208 -lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
   3.209 -by (auto simp: Sup_prod_def SUP_def)
   3.210 -
   3.211 -lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
   3.212 -by (auto simp: INF_def Inf_prod_def image_compose)
   3.213 -
   3.214 -lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
   3.215 -by (auto simp: SUP_def Sup_prod_def image_compose)
   3.216 -
   3.217 -lemma INF_prod_alt_def:
   3.218 -  "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
   3.219 -by (metis fst_INF snd_INF surjective_pairing)
   3.220 -
   3.221 -lemma SUP_prod_alt_def:
   3.222 -  "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
   3.223 -by (metis fst_SUP snd_SUP surjective_pairing)
   3.224 -
   3.225 -
   3.226 -subsection {* Complete distributive lattices *}
   3.227 -
   3.228 -(* Contribution: Alessandro Coglio *)
   3.229 -
   3.230 -instance prod ::
   3.231 -  (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
   3.232 -proof
   3.233 -  case goal1 thus ?case
   3.234 -    by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF)
   3.235 -next
   3.236 -  case goal2 thus ?case
   3.237 -    by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP)
   3.238 -qed
   3.239 -
   3.240 -
   3.241 -end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Product_Lexorder.thy	Thu Feb 14 16:01:59 2013 +0100
     4.3 @@ -0,0 +1,125 @@
     4.4 +(*  Title:      HOL/Library/Product_Lexorder.thy
     4.5 +    Author:     Norbert Voelker
     4.6 +*)
     4.7 +
     4.8 +header {* Lexicographic order on product types *}
     4.9 +
    4.10 +theory Product_Lexorder
    4.11 +imports Main
    4.12 +begin
    4.13 +
    4.14 +instantiation prod :: (ord, ord) ord
    4.15 +begin
    4.16 +
    4.17 +definition
    4.18 +  "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
    4.19 +
    4.20 +definition
    4.21 +  "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
    4.22 +
    4.23 +instance ..
    4.24 +
    4.25 +end
    4.26 +
    4.27 +lemma less_eq_prod_simp [simp, code]:
    4.28 +  "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
    4.29 +  by (simp add: less_eq_prod_def)
    4.30 +
    4.31 +lemma less_prod_simp [simp, code]:
    4.32 +  "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
    4.33 +  by (simp add: less_prod_def)
    4.34 +
    4.35 +text {* A stronger version for partial orders. *}
    4.36 +
    4.37 +lemma less_prod_def':
    4.38 +  fixes x y :: "'a::order \<times> 'b::ord"
    4.39 +  shows "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
    4.40 +  by (auto simp add: less_prod_def le_less)
    4.41 +
    4.42 +instance prod :: (preorder, preorder) preorder
    4.43 +  by default (auto simp: less_eq_prod_def less_prod_def less_le_not_le intro: order_trans)
    4.44 +
    4.45 +instance prod :: (order, order) order
    4.46 +  by default (auto simp add: less_eq_prod_def)
    4.47 +
    4.48 +instance prod :: (linorder, linorder) linorder
    4.49 +  by default (auto simp: less_eq_prod_def)
    4.50 +
    4.51 +instantiation prod :: (linorder, linorder) distrib_lattice
    4.52 +begin
    4.53 +
    4.54 +definition
    4.55 +  "(inf :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
    4.56 +
    4.57 +definition
    4.58 +  "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
    4.59 +
    4.60 +instance
    4.61 +  by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
    4.62 +
    4.63 +end
    4.64 +
    4.65 +instantiation prod :: (bot, bot) bot
    4.66 +begin
    4.67 +
    4.68 +definition
    4.69 +  "bot = (bot, bot)"
    4.70 +
    4.71 +instance
    4.72 +  by default (auto simp add: bot_prod_def)
    4.73 +
    4.74 +end
    4.75 +
    4.76 +instantiation prod :: (top, top) top
    4.77 +begin
    4.78 +
    4.79 +definition
    4.80 +  "top = (top, top)"
    4.81 +
    4.82 +instance
    4.83 +  by default (auto simp add: top_prod_def)
    4.84 +
    4.85 +end
    4.86 +
    4.87 +instance prod :: (wellorder, wellorder) wellorder
    4.88 +proof
    4.89 +  fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"
    4.90 +  assume P: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
    4.91 +  show "P z"
    4.92 +  proof (induct z)
    4.93 +    case (Pair a b)
    4.94 +    show "P (a, b)"
    4.95 +    proof (induct a arbitrary: b rule: less_induct)
    4.96 +      case (less a\<^isub>1) note a\<^isub>1 = this
    4.97 +      show "P (a\<^isub>1, b)"
    4.98 +      proof (induct b rule: less_induct)
    4.99 +        case (less b\<^isub>1) note b\<^isub>1 = this
   4.100 +        show "P (a\<^isub>1, b\<^isub>1)"
   4.101 +        proof (rule P)
   4.102 +          fix p assume p: "p < (a\<^isub>1, b\<^isub>1)"
   4.103 +          show "P p"
   4.104 +          proof (cases "fst p < a\<^isub>1")
   4.105 +            case True
   4.106 +            then have "P (fst p, snd p)" by (rule a\<^isub>1)
   4.107 +            then show ?thesis by simp
   4.108 +          next
   4.109 +            case False
   4.110 +            with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1"
   4.111 +              by (simp_all add: less_prod_def')
   4.112 +            from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1)
   4.113 +            with 1 show ?thesis by simp
   4.114 +          qed
   4.115 +        qed
   4.116 +      qed
   4.117 +    qed
   4.118 +  qed
   4.119 +qed
   4.120 +
   4.121 +text {* Legacy lemma bindings *}
   4.122 +
   4.123 +lemmas prod_le_def = less_eq_prod_def
   4.124 +lemmas prod_less_def = less_prod_def
   4.125 +lemmas prod_less_eq = less_prod_def'
   4.126 +
   4.127 +end
   4.128 +
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/Product_Order.thy	Thu Feb 14 16:01:59 2013 +0100
     5.3 @@ -0,0 +1,238 @@
     5.4 +(*  Title:      HOL/Library/Product_Order.thy
     5.5 +    Author:     Brian Huffman
     5.6 +*)
     5.7 +
     5.8 +header {* Pointwise order on product types *}
     5.9 +
    5.10 +theory Product_Order
    5.11 +imports "~~/src/HOL/Library/Product_plus"
    5.12 +begin
    5.13 +
    5.14 +subsection {* Pointwise ordering *}
    5.15 +
    5.16 +instantiation prod :: (ord, ord) ord
    5.17 +begin
    5.18 +
    5.19 +definition
    5.20 +  "x \<le> y \<longleftrightarrow> fst x \<le> fst y \<and> snd x \<le> snd y"
    5.21 +
    5.22 +definition
    5.23 +  "(x::'a \<times> 'b) < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
    5.24 +
    5.25 +instance ..
    5.26 +
    5.27 +end
    5.28 +
    5.29 +lemma fst_mono: "x \<le> y \<Longrightarrow> fst x \<le> fst y"
    5.30 +  unfolding less_eq_prod_def by simp
    5.31 +
    5.32 +lemma snd_mono: "x \<le> y \<Longrightarrow> snd x \<le> snd y"
    5.33 +  unfolding less_eq_prod_def by simp
    5.34 +
    5.35 +lemma Pair_mono: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> (x, y) \<le> (x', y')"
    5.36 +  unfolding less_eq_prod_def by simp
    5.37 +
    5.38 +lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d"
    5.39 +  unfolding less_eq_prod_def by simp
    5.40 +
    5.41 +instance prod :: (preorder, preorder) preorder
    5.42 +proof
    5.43 +  fix x y z :: "'a \<times> 'b"
    5.44 +  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
    5.45 +    by (rule less_prod_def)
    5.46 +  show "x \<le> x"
    5.47 +    unfolding less_eq_prod_def
    5.48 +    by fast
    5.49 +  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
    5.50 +    unfolding less_eq_prod_def
    5.51 +    by (fast elim: order_trans)
    5.52 +qed
    5.53 +
    5.54 +instance prod :: (order, order) order
    5.55 +  by default auto
    5.56 +
    5.57 +
    5.58 +subsection {* Binary infimum and supremum *}
    5.59 +
    5.60 +instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf
    5.61 +begin
    5.62 +
    5.63 +definition
    5.64 +  "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
    5.65 +
    5.66 +lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
    5.67 +  unfolding inf_prod_def by simp
    5.68 +
    5.69 +lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)"
    5.70 +  unfolding inf_prod_def by simp
    5.71 +
    5.72 +lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
    5.73 +  unfolding inf_prod_def by simp
    5.74 +
    5.75 +instance
    5.76 +  by default auto
    5.77 +
    5.78 +end
    5.79 +
    5.80 +instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup
    5.81 +begin
    5.82 +
    5.83 +definition
    5.84 +  "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))"
    5.85 +
    5.86 +lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)"
    5.87 +  unfolding sup_prod_def by simp
    5.88 +
    5.89 +lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)"
    5.90 +  unfolding sup_prod_def by simp
    5.91 +
    5.92 +lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
    5.93 +  unfolding sup_prod_def by simp
    5.94 +
    5.95 +instance
    5.96 +  by default auto
    5.97 +
    5.98 +end
    5.99 +
   5.100 +instance prod :: (lattice, lattice) lattice ..
   5.101 +
   5.102 +instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
   5.103 +  by default (auto simp add: sup_inf_distrib1)
   5.104 +
   5.105 +
   5.106 +subsection {* Top and bottom elements *}
   5.107 +
   5.108 +instantiation prod :: (top, top) top
   5.109 +begin
   5.110 +
   5.111 +definition
   5.112 +  "top = (top, top)"
   5.113 +
   5.114 +lemma fst_top [simp]: "fst top = top"
   5.115 +  unfolding top_prod_def by simp
   5.116 +
   5.117 +lemma snd_top [simp]: "snd top = top"
   5.118 +  unfolding top_prod_def by simp
   5.119 +
   5.120 +lemma Pair_top_top: "(top, top) = top"
   5.121 +  unfolding top_prod_def by simp
   5.122 +
   5.123 +instance
   5.124 +  by default (auto simp add: top_prod_def)
   5.125 +
   5.126 +end
   5.127 +
   5.128 +instantiation prod :: (bot, bot) bot
   5.129 +begin
   5.130 +
   5.131 +definition
   5.132 +  "bot = (bot, bot)"
   5.133 +
   5.134 +lemma fst_bot [simp]: "fst bot = bot"
   5.135 +  unfolding bot_prod_def by simp
   5.136 +
   5.137 +lemma snd_bot [simp]: "snd bot = bot"
   5.138 +  unfolding bot_prod_def by simp
   5.139 +
   5.140 +lemma Pair_bot_bot: "(bot, bot) = bot"
   5.141 +  unfolding bot_prod_def by simp
   5.142 +
   5.143 +instance
   5.144 +  by default (auto simp add: bot_prod_def)
   5.145 +
   5.146 +end
   5.147 +
   5.148 +instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
   5.149 +
   5.150 +instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
   5.151 +  by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
   5.152 +
   5.153 +
   5.154 +subsection {* Complete lattice operations *}
   5.155 +
   5.156 +instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
   5.157 +begin
   5.158 +
   5.159 +definition
   5.160 +  "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
   5.161 +
   5.162 +definition
   5.163 +  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
   5.164 +
   5.165 +instance
   5.166 +  by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
   5.167 +    INF_lower SUP_upper le_INF_iff SUP_le_iff)
   5.168 +
   5.169 +end
   5.170 +
   5.171 +lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
   5.172 +  unfolding Sup_prod_def by simp
   5.173 +
   5.174 +lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
   5.175 +  unfolding Sup_prod_def by simp
   5.176 +
   5.177 +lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
   5.178 +  unfolding Inf_prod_def by simp
   5.179 +
   5.180 +lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
   5.181 +  unfolding Inf_prod_def by simp
   5.182 +
   5.183 +lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
   5.184 +  by (simp add: SUP_def fst_Sup image_image)
   5.185 +
   5.186 +lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
   5.187 +  by (simp add: SUP_def snd_Sup image_image)
   5.188 +
   5.189 +lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
   5.190 +  by (simp add: INF_def fst_Inf image_image)
   5.191 +
   5.192 +lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
   5.193 +  by (simp add: INF_def snd_Inf image_image)
   5.194 +
   5.195 +lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
   5.196 +  by (simp add: SUP_def Sup_prod_def image_image)
   5.197 +
   5.198 +lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
   5.199 +  by (simp add: INF_def Inf_prod_def image_image)
   5.200 +
   5.201 +
   5.202 +text {* Alternative formulations for set infima and suprema over the product
   5.203 +of two complete lattices: *}
   5.204 +
   5.205 +lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
   5.206 +by (auto simp: Inf_prod_def INF_def)
   5.207 +
   5.208 +lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
   5.209 +by (auto simp: Sup_prod_def SUP_def)
   5.210 +
   5.211 +lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
   5.212 +by (auto simp: INF_def Inf_prod_def image_compose)
   5.213 +
   5.214 +lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
   5.215 +by (auto simp: SUP_def Sup_prod_def image_compose)
   5.216 +
   5.217 +lemma INF_prod_alt_def:
   5.218 +  "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
   5.219 +by (metis fst_INF snd_INF surjective_pairing)
   5.220 +
   5.221 +lemma SUP_prod_alt_def:
   5.222 +  "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
   5.223 +by (metis fst_SUP snd_SUP surjective_pairing)
   5.224 +
   5.225 +
   5.226 +subsection {* Complete distributive lattices *}
   5.227 +
   5.228 +(* Contribution: Alessandro Coglio *)
   5.229 +
   5.230 +instance prod ::
   5.231 +  (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
   5.232 +proof
   5.233 +  case goal1 thus ?case
   5.234 +    by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF)
   5.235 +next
   5.236 +  case goal2 thus ?case
   5.237 +    by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP)
   5.238 +qed
   5.239 +
   5.240 +end
   5.241 +
     6.1 --- a/src/HOL/Library/Product_ord.thy	Thu Feb 14 16:01:28 2013 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,115 +0,0 @@
     6.4 -(*  Title:      HOL/Library/Product_ord.thy
     6.5 -    Author:     Norbert Voelker
     6.6 -*)
     6.7 -
     6.8 -header {* Order on product types *}
     6.9 -
    6.10 -theory Product_ord
    6.11 -imports Main
    6.12 -begin
    6.13 -
    6.14 -instantiation prod :: (ord, ord) ord
    6.15 -begin
    6.16 -
    6.17 -definition
    6.18 -  prod_le_def: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
    6.19 -
    6.20 -definition
    6.21 -  prod_less_def: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
    6.22 -
    6.23 -instance ..
    6.24 -
    6.25 -end
    6.26 -
    6.27 -lemma [code]:
    6.28 -  "(x1::'a::{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
    6.29 -  "(x1::'a::{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
    6.30 -  unfolding prod_le_def prod_less_def by simp_all
    6.31 -
    6.32 -instance prod :: (preorder, preorder) preorder
    6.33 -  by default (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
    6.34 -
    6.35 -instance prod :: (order, order) order
    6.36 -  by default (auto simp add: prod_le_def)
    6.37 -
    6.38 -instance prod :: (linorder, linorder) linorder
    6.39 -  by default (auto simp: prod_le_def)
    6.40 -
    6.41 -instantiation prod :: (linorder, linorder) distrib_lattice
    6.42 -begin
    6.43 -
    6.44 -definition
    6.45 -  inf_prod_def: "(inf :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
    6.46 -
    6.47 -definition
    6.48 -  sup_prod_def: "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
    6.49 -
    6.50 -instance
    6.51 -  by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
    6.52 -
    6.53 -end
    6.54 -
    6.55 -instantiation prod :: (bot, bot) bot
    6.56 -begin
    6.57 -
    6.58 -definition
    6.59 -  bot_prod_def: "bot = (bot, bot)"
    6.60 -
    6.61 -instance
    6.62 -  by default (auto simp add: bot_prod_def prod_le_def)
    6.63 -
    6.64 -end
    6.65 -
    6.66 -instantiation prod :: (top, top) top
    6.67 -begin
    6.68 -
    6.69 -definition
    6.70 -  top_prod_def: "top = (top, top)"
    6.71 -
    6.72 -instance
    6.73 -  by default (auto simp add: top_prod_def prod_le_def)
    6.74 -
    6.75 -end
    6.76 -
    6.77 -text {* A stronger version of the definition holds for partial orders. *}
    6.78 -
    6.79 -lemma prod_less_eq:
    6.80 -  fixes x y :: "'a::order \<times> 'b::ord"
    6.81 -  shows "x < y \<longleftrightarrow> fst x < fst y \<or> (fst x = fst y \<and> snd x < snd y)"
    6.82 -  unfolding prod_less_def fst_conv snd_conv le_less by auto
    6.83 -
    6.84 -instance prod :: (wellorder, wellorder) wellorder
    6.85 -proof
    6.86 -  fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"
    6.87 -  assume P: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
    6.88 -  show "P z"
    6.89 -  proof (induct z)
    6.90 -    case (Pair a b)
    6.91 -    show "P (a, b)"
    6.92 -    proof (induct a arbitrary: b rule: less_induct)
    6.93 -      case (less a\<^isub>1) note a\<^isub>1 = this
    6.94 -      show "P (a\<^isub>1, b)"
    6.95 -      proof (induct b rule: less_induct)
    6.96 -        case (less b\<^isub>1) note b\<^isub>1 = this
    6.97 -        show "P (a\<^isub>1, b\<^isub>1)"
    6.98 -        proof (rule P)
    6.99 -          fix p assume p: "p < (a\<^isub>1, b\<^isub>1)"
   6.100 -          show "P p"
   6.101 -          proof (cases "fst p < a\<^isub>1")
   6.102 -            case True
   6.103 -            then have "P (fst p, snd p)" by (rule a\<^isub>1)
   6.104 -            then show ?thesis by simp
   6.105 -          next
   6.106 -            case False
   6.107 -            with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1"
   6.108 -              by (simp_all add: prod_less_eq)
   6.109 -            from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1)
   6.110 -            with 1 show ?thesis by simp
   6.111 -          qed
   6.112 -        qed
   6.113 -      qed
   6.114 -    qed
   6.115 -  qed
   6.116 -qed
   6.117 -
   6.118 -end
     7.1 --- a/src/HOL/Library/RBT_Set.thy	Thu Feb 14 16:01:28 2013 +0100
     7.2 +++ b/src/HOL/Library/RBT_Set.thy	Thu Feb 14 16:01:59 2013 +0100
     7.3 @@ -5,7 +5,7 @@
     7.4  header {* Implementation of sets using RBT trees *}
     7.5  
     7.6  theory RBT_Set
     7.7 -imports RBT Product_ord
     7.8 +imports RBT Product_Lexorder
     7.9  begin
    7.10  
    7.11  (*
     8.1 --- a/src/HOL/ROOT	Thu Feb 14 16:01:28 2013 +0100
     8.2 +++ b/src/HOL/ROOT	Thu Feb 14 16:01:59 2013 +0100
     8.3 @@ -26,6 +26,8 @@
     8.4      Finite_Lattice
     8.5      Code_Char_chr
     8.6      Code_Char_ord
     8.7 +    Product_Lexorder
     8.8 +    Product_Order
     8.9      Code_Integer
    8.10      Efficient_Nat
    8.11      (* Code_Prolog  FIXME cf. 76965c356d2a *)