blob: bcf4348b5cc5d98a93f3985dcfddffd12225e212 (
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
|
(*Generated by Lem from maybe.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_boolTheory lem_basic_classesTheory lem_functionTheory;
val _ = numLib.prefer_num();
val _ = new_theory "lem_maybe"
(*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*)
val _ = Define `
((maybeEqualBy:('a -> 'a -> bool) -> 'a option -> 'a option -> bool) eq NONE NONE= T)
/\ ((maybeEqualBy:('a -> 'a -> bool) -> 'a option -> 'a option -> bool) eq NONE (SOME _)= F)
/\ ((maybeEqualBy:('a -> 'a -> bool) -> 'a option -> 'a option -> bool) eq (SOME _) NONE= F)
/\ ((maybeEqualBy:('a -> 'a -> bool) -> 'a option -> 'a option -> bool) eq (SOME x') (SOME y')= (eq x' y'))`;
val _ = Define `
((maybeCompare:('b -> 'a -> ordering) -> 'b option -> 'a option -> ordering) cmp NONE NONE= EQUAL)
/\ ((maybeCompare:('b -> 'a -> ordering) -> 'b option -> 'a option -> ordering) cmp NONE (SOME _)= LESS)
/\ ((maybeCompare:('b -> 'a -> ordering) -> 'b option -> 'a option -> ordering) cmp (SOME _) NONE= GREATER)
/\ ((maybeCompare:('b -> 'a -> ordering) -> 'b option -> 'a option -> ordering) cmp (SOME x') (SOME y')= (cmp x' y'))`;
val _ = Define `
((instance_Basic_classes_Ord_Maybe_maybe_dict:'a Ord_class ->('a option)Ord_class)dict_Basic_classes_Ord_a= (<|
compare_method := (maybeCompare
dict_Basic_classes_Ord_a.compare_method);
isLess_method := (\ m1 . (\ m2 . maybeCompare
dict_Basic_classes_Ord_a.compare_method m1 m2 = LESS));
isLessEqual_method := (\ m1 . (\ m2 . (let r = (maybeCompare
dict_Basic_classes_Ord_a.compare_method m1 m2) in (r = LESS) \/ (r = EQUAL))));
isGreater_method := (\ m1 . (\ m2 . maybeCompare
dict_Basic_classes_Ord_a.compare_method m1 m2 = GREATER));
isGreaterEqual_method := (\ m1 . (\ m2 . (let r = (maybeCompare
dict_Basic_classes_Ord_a.compare_method m1 m2) in (r = GREATER) \/ (r = EQUAL))))|>))`;
(* ----------------------- *)
(* 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*)
val _ = export_theory()
|
