src/HOL/Library/Product_Order.thy
changeset 62053 1c8252d07e32
parent 61166 5976fe402824
child 62343 24106dc44def
equal deleted inserted replaced
62052:8bcbf1c93119 62053:1c8252d07e32
   151   by standard (auto simp add: bot_prod_def)
   151   by standard (auto simp add: bot_prod_def)
   152 
   152 
   153 instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
   153 instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
   154 
   154 
   155 instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
   155 instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
   156   by standard (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
   156   by standard (auto simp add: prod_eqI diff_eq)
   157 
   157 
   158 
   158 
   159 subsection \<open>Complete lattice operations\<close>
   159 subsection \<open>Complete lattice operations\<close>
   160 
   160 
   161 instantiation prod :: (Inf, Inf) Inf
   161 instantiation prod :: (Inf, Inf) Inf
   177 end
   177 end
   178 
   178 
   179 instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
   179 instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
   180     conditionally_complete_lattice
   180     conditionally_complete_lattice
   181   by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
   181   by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
   182     INF_def SUP_def simp del: Inf_image_eq Sup_image_eq intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
   182     INF_def SUP_def simp del: Inf_image_eq Sup_image_eq
       
   183     intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
   183 
   184 
   184 instance prod :: (complete_lattice, complete_lattice) complete_lattice
   185 instance prod :: (complete_lattice, complete_lattice) complete_lattice
   185   by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
   186   by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
   186     INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
   187     INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
   187 
   188