src/HOL/Library/Product_Order.thy
changeset 67829 2a6ef5ba4822
parent 67091 1393c2340eec
child 69260 0a9688695a1b
     1.1 --- a/src/HOL/Library/Product_Order.thy	Mon Mar 12 08:25:35 2018 +0000
     1.2 +++ b/src/HOL/Library/Product_Order.thy	Mon Mar 12 20:52:53 2018 +0100
     1.3 @@ -233,14 +233,10 @@
     1.4  (* Contribution: Alessandro Coglio *)
     1.5  
     1.6  instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
     1.7 -proof (standard, goal_cases)
     1.8 -  case 1
     1.9 -  then show ?case
    1.10 -    by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
    1.11 -next
    1.12 -  case 2
    1.13 -  then show ?case
    1.14 -    by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP comp_def)
    1.15 +proof
    1.16 +  fix A::"('a\<times>'b) set set"
    1.17 +  show "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
    1.18 +    by (simp add: Sup_prod_def Inf_prod_def INF_SUP_set)
    1.19  qed
    1.20  
    1.21  subsection \<open>Bekic's Theorem\<close>