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