src/HOL/Library/Extended_Real.thy
changeset 52729 412c9e0381a1
parent 51775 408d937c9486
child 53216 ad2e09c30aa8
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Jul 24 17:15:59 2013 +0200
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Jul 25 08:57:16 2013 +0200
     1.3 @@ -1144,8 +1144,22 @@
     1.4    using ereal_complete_Sup[of "uminus ` S"] unfolding ereal_complete_uminus_eq by auto
     1.5  
     1.6  instance
     1.7 -  by default (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
     1.8 -                   simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
     1.9 +proof
    1.10 +  show "Sup {} = (bot::ereal)"
    1.11 +  apply (auto simp: bot_ereal_def Sup_ereal_def)
    1.12 +  apply (rule some1_equality)
    1.13 +  apply (metis ereal_bot ereal_less_eq(2))
    1.14 +  apply (metis ereal_less_eq(2))
    1.15 +  done
    1.16 +next
    1.17 +  show "Inf {} = (top::ereal)"
    1.18 +  apply (auto simp: top_ereal_def Inf_ereal_def)
    1.19 +  apply (rule some1_equality)
    1.20 +  apply (metis ereal_top ereal_less_eq(1))
    1.21 +  apply (metis ereal_less_eq(1))
    1.22 +  done
    1.23 +qed (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
    1.24 +  simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
    1.25  
    1.26  end
    1.27