src/HOL/Library/Product_Order.thy
changeset 62343 24106dc44def
parent 62053 1c8252d07e32
child 63561 fba08009ff3e
     1.1 --- a/src/HOL/Library/Product_Order.thy	Wed Feb 17 21:51:55 2016 +0100
     1.2 +++ b/src/HOL/Library/Product_Order.thy	Wed Feb 17 21:51:56 2016 +0100
     1.3 @@ -179,7 +179,6 @@
     1.4  instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
     1.5      conditionally_complete_lattice
     1.6    by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
     1.7 -    INF_def SUP_def simp del: Inf_image_eq Sup_image_eq
     1.8      intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
     1.9  
    1.10  instance prod :: (complete_lattice, complete_lattice) complete_lattice
    1.11 @@ -211,10 +210,10 @@
    1.12    using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def)
    1.13  
    1.14  lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
    1.15 -  unfolding SUP_def Sup_prod_def by (simp add: comp_def)
    1.16 +  unfolding Sup_prod_def by (simp add: comp_def)
    1.17  
    1.18  lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
    1.19 -  unfolding INF_def Inf_prod_def by (simp add: comp_def)
    1.20 +  unfolding Inf_prod_def by (simp add: comp_def)
    1.21  
    1.22  
    1.23  text \<open>Alternative formulations for set infima and suprema over the product
    1.24 @@ -222,11 +221,11 @@
    1.25  
    1.26  lemma INF_prod_alt_def:
    1.27    "INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))"
    1.28 -  unfolding INF_def Inf_prod_def by simp
    1.29 +  unfolding Inf_prod_def by simp
    1.30  
    1.31  lemma SUP_prod_alt_def:
    1.32    "SUPREMUM A f = (SUPREMUM A (fst o f), SUPREMUM A (snd o f))"
    1.33 -  unfolding SUP_def Sup_prod_def by simp
    1.34 +  unfolding Sup_prod_def by simp
    1.35  
    1.36  
    1.37  subsection \<open>Complete distributive lattices\<close>