blob: da0bde92218fa2c5bb841a3d2ed3765107eada59 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
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
|
