1 files changed, 113 insertions, 0 deletions
diff --git a/snapshots/isabelle/lib/lem/Lem_maybe.thy b/snapshots/isabelle/lib/lem/Lem_maybe.thy
new file mode 100644
index 00000000..da0bde92
--- /dev/null
+++ b/snapshots/isabelle/lib/lem/Lem_maybe.thy
@@ -0,0 +1,113 @@
+chapter \<open>Generated by Lem from maybe.lem.\<close>
+
+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 \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow> 'a option \<Rightarrow> 'a option \<Rightarrow> 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 \<Rightarrow> 'a \<Rightarrow> ordering)\<Rightarrow> 'b option \<Rightarrow> 'a option \<Rightarrow> 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 \<Rightarrow>('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 = (\<lambda> m1 .  (\<lambda> m2 .  maybeCompare 
+  (compare_method   dict_Basic_classes_Ord_a) m1 m2 = LT)),
+
+  isLessEqual_method = (\<lambda> m1 .  (\<lambda> m2 .  ((let r = (maybeCompare 
+  (compare_method   dict_Basic_classes_Ord_a) m1 m2) in (r = LT) \<or> (r = EQ))))),
+
+  isGreater_method = (\<lambda> m1 .  (\<lambda> m2 .  maybeCompare 
+  (compare_method   dict_Basic_classes_Ord_a) m1 m2 = GT)),
+
+  isGreaterEqual_method = (\<lambda> m1 .  (\<lambda> m2 .  ((let r = (maybeCompare 
+  (compare_method   dict_Basic_classes_Ord_a) m1 m2) in (r = GT) \<or> (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