src/HOL/Library/Option_ord.thy
changeset 69313 b021008c5397
parent 68980 5717fbc55521
child 69661 a03a63b81f44
     1.1 --- a/src/HOL/Library/Option_ord.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Library/Option_ord.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -283,7 +283,8 @@
     1.4    "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
     1.5    using Some_Sup [of "f ` A"] by (simp add: comp_def)
     1.6  
     1.7 -lemma option_Inf_Sup: "INFIMUM (A::('a::complete_distrib_lattice option) set set) Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
     1.8 +lemma option_Inf_Sup: "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
     1.9 +  for A :: "('a::complete_distrib_lattice option) set set"
    1.10  proof (cases "{} \<in> A")
    1.11    case True
    1.12    then show ?thesis
    1.13 @@ -438,8 +439,8 @@
    1.14      also have "... = Some (\<Squnion>x\<in>{f ` {the ` (y - {None}) |y. y \<in> A} |f. \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y}. \<Sqinter>x) "
    1.15        by (simp add: Inf_Sup)
    1.16    
    1.17 -    also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
    1.18 -    proof (cases "SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf")
    1.19 +    also have "... \<le> \<Squnion> (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
    1.20 +    proof (cases "\<Squnion> (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})")
    1.21        case None
    1.22        then show ?thesis by (simp add: less_eq_option_def)
    1.23      next