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