src/HOL/Library/Product_Order.thy
 changeset 54776 db890d9fc5c2 parent 52729 412c9e0381a1 child 56154 f0a927235162
```     1.1 --- a/src/HOL/Library/Product_Order.thy	Mon Dec 16 17:08:22 2013 +0100
1.2 +++ b/src/HOL/Library/Product_Order.thy	Mon Dec 16 17:08:22 2013 +0100
1.3 @@ -5,7 +5,7 @@
1.4  header {* Pointwise order on product types *}
1.5
1.6  theory Product_Order
1.7 -imports Product_plus
1.8 +imports Product_plus Conditionally_Complete_Lattices
1.9  begin
1.10
1.11  subsection {* Pointwise ordering *}
1.12 @@ -54,7 +54,7 @@
1.13
1.14  subsection {* Binary infimum and supremum *}
1.15
1.16 -instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf
1.17 +instantiation prod :: (inf, inf) inf
1.18  begin
1.19
1.20  definition
1.21 @@ -69,12 +69,14 @@
1.22  lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
1.23    unfolding inf_prod_def by simp
1.24
1.25 -instance
1.26 +instance proof qed
1.27 +end
1.28 +
1.29 +instance prod :: (semilattice_inf, semilattice_inf) semilattice_inf
1.30    by default auto
1.31
1.32 -end
1.33
1.34 -instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup
1.35 +instantiation prod :: (sup, sup) sup
1.36  begin
1.37
1.38  definition
1.39 @@ -89,11 +91,12 @@
1.40  lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
1.41    unfolding sup_prod_def by simp
1.42
1.43 -instance
1.44 +instance proof qed
1.45 +end
1.46 +
1.47 +instance prod :: (semilattice_sup, semilattice_sup) semilattice_sup
1.48    by default auto
1.49
1.50 -end
1.51 -
1.52  instance prod :: (lattice, lattice) lattice ..
1.53
1.54  instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
1.55 @@ -154,21 +157,33 @@
1.56
1.57  subsection {* Complete lattice operations *}
1.58
1.59 -instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
1.60 +instantiation prod :: (Inf, Inf) Inf
1.61 +begin
1.62 +
1.63 +definition
1.64 +  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
1.65 +
1.66 +instance proof qed
1.67 +end
1.68 +
1.69 +instantiation prod :: (Sup, Sup) Sup
1.70  begin
1.71
1.72  definition
1.73    "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
1.74
1.75 -definition
1.76 -  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
1.77 +instance proof qed
1.78 +end
1.79
1.80 -instance
1.81 +instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
1.82 +    conditionally_complete_lattice
1.83 +  by default (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
1.84 +    INF_def SUP_def intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
1.85 +
1.86 +instance prod :: (complete_lattice, complete_lattice) complete_lattice
1.87    by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
1.88      INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
1.89
1.90 -end
1.91 -
1.92  lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
1.93    unfolding Sup_prod_def by simp
1.94
```