src/HOL/Library/Option_ord.thy
changeset 52729 412c9e0381a1
parent 49190 e1e1d427747d
child 56166 9a241bc276cd
     1.1 --- a/src/HOL/Library/Option_ord.thy	Wed Jul 24 17:15:59 2013 +0200
     1.2 +++ b/src/HOL/Library/Option_ord.thy	Thu Jul 25 08:57:16 2013 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4  instance option :: (linorder) linorder proof
     1.5  qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
     1.6  
     1.7 -instantiation option :: (order) bot
     1.8 +instantiation option :: (order) order_bot
     1.9  begin
    1.10  
    1.11  definition bot_option where
    1.12 @@ -84,7 +84,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -instantiation option :: (top) top
    1.17 +instantiation option :: (order_top) order_top
    1.18  begin
    1.19  
    1.20  definition top_option where
    1.21 @@ -272,6 +272,12 @@
    1.22      then have "\<Squnion>Option.these A \<le> y" by (rule Sup_least)
    1.23      with Some show ?thesis by (simp add: Sup_option_def)
    1.24    qed
    1.25 +next
    1.26 +  show "\<Squnion>{} = (\<bottom>::'a option)"
    1.27 +  by (auto simp: bot_option_def)
    1.28 +next
    1.29 +  show "\<Sqinter>{} = (\<top>::'a option)"
    1.30 +  by (auto simp: top_option_def Inf_option_def)
    1.31  qed
    1.32  
    1.33  end