Theory Lem_maybe

chapter ‹Generated by Lem from maybe.lem›.›

theory "Lem_maybe" 

imports
  Main
  "Lem_bool"
  "Lem_basic_classes"
  "Lem_function"

begin 

 

― ‹open import Bool Basic_classes Function›

― ‹ ========================================================================== ›
― ‹ Basic stuff                                                                ›
― ‹ ========================================================================== ›

― ‹type maybe 'a = 
  | Nothing
  | Just of 'a›


― ‹val maybeEqual : forall 'a. Eq 'a => maybe 'a -> maybe 'a -> bool›
― ‹val maybeEqualBy : forall 'a. ('a -> 'a -> bool) -> maybe 'a -> maybe 'a -> bool›

fun maybeEqualBy  :: "('a  'a  bool) 'a option  'a option  bool "  where 
     " maybeEqualBy eq None None = ( True )"
|" maybeEqualBy eq None (Some _) = ( False )"
|" maybeEqualBy eq (Some _) None = ( False )"
|" maybeEqualBy eq (Some x') (Some y') = ( (eq x' y'))"
  


fun maybeCompare  :: "('b  'a  ordering) 'b option  'a option  ordering "  where 
     " maybeCompare cmp None None = ( EQ )"
|" maybeCompare cmp None (Some _) = ( LT )"
|" maybeCompare cmp (Some _) None = ( GT )"
|" maybeCompare cmp (Some x') (Some y') = ( cmp x' y' )"


definition instance_Basic_classes_Ord_Maybe_maybe_dict  :: " 'a Ord_class ('a option)Ord_class "  where 
     " instance_Basic_classes_Ord_Maybe_maybe_dict dict_Basic_classes_Ord_a = ((|

  compare_method = (maybeCompare 
  (compare_method   dict_Basic_classes_Ord_a)),

  isLess_method = (λ m1 .  (λ m2 .  maybeCompare 
  (compare_method   dict_Basic_classes_Ord_a) m1 m2 = LT)),

  isLessEqual_method = (λ m1 .  (λ m2 .  ((let r = (maybeCompare 
  (compare_method   dict_Basic_classes_Ord_a) m1 m2) in (r = LT)  (r = EQ))))),

  isGreater_method = (λ m1 .  (λ m2 .  maybeCompare 
  (compare_method   dict_Basic_classes_Ord_a) m1 m2 = GT)),

  isGreaterEqual_method = (λ m1 .  (λ m2 .  ((let r = (maybeCompare 
  (compare_method   dict_Basic_classes_Ord_a) m1 m2) in (r = GT)  (r = EQ)))))|) )"


― ‹ ----------------------- ›
― ‹ maybe                   ›
― ‹ ----------------------- ›

― ‹val maybe : forall 'a 'b. 'b -> ('a -> 'b) -> maybe 'a -> 'b›
― ‹let maybe d f mb=  match mb with 
  | Just a -> f a
  | Nothing -> d
end›

― ‹ ----------------------- ›
― ‹ isJust / isNothing      ›
― ‹ ----------------------- ›

― ‹val isJust : forall 'a. maybe 'a -> bool›
― ‹let isJust mb=  match mb with 
  | Just _ -> true
  | Nothing -> false
end›

― ‹val isNothing : forall 'a. maybe 'a -> bool›
― ‹let isNothing mb=  match mb with 
  | Just _ -> false
  | Nothing -> true
end›

― ‹ ----------------------- ›
― ‹ fromMaybe               ›
― ‹ ----------------------- ›

― ‹val fromMaybe : forall 'a. 'a -> maybe 'a -> 'a›
― ‹let fromMaybe d mb=  match mb with
   | Just v  -> v
   | Nothing -> d
end›

― ‹ ----------------------- ›
― ‹ map                     ›
― ‹ ----------------------- ›

― ‹val map : forall 'a 'b. ('a -> 'b) -> maybe 'a -> maybe 'b› 
― ‹let map f=  maybe Nothing (fun v -> Just (f v))›


― ‹ ----------------------- ›
― ‹ bind                    ›
― ‹ ----------------------- ›

― ‹val bind : forall 'a 'b. maybe 'a -> ('a -> maybe 'b) -> maybe 'b› 
― ‹let bind mb f=  maybe Nothing f mb›
end