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
|
(*Generated by Lem from either.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_boolTheory lem_basic_classesTheory lem_listTheory lem_tupleTheory sumTheory;
val _ = numLib.prefer_num();
val _ = new_theory "lem_either"
(*open import Bool Basic_classes List Tuple*)
(*open import {hol} `sumTheory`*)
(*open import {ocaml} `Either`*)
(*type either 'a 'b
= Left of 'a
| Right of 'b*)
(* -------------------------------------------------------------------------- *)
(* Equality. *)
(* -------------------------------------------------------------------------- *)
(*val eitherEqual : forall 'a 'b. Eq 'a, Eq 'b => (either 'a 'b) -> (either 'a 'b) -> bool*)
(*val eitherEqualBy : forall 'a 'b. ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> (either 'a 'b) -> (either 'a 'b) -> bool*)
val _ = Define `
((eitherEqualBy:('a -> 'a -> bool) ->('b -> 'b -> bool) ->('a,'b)sum ->('a,'b)sum -> bool) eql eqr (left: ('a, 'b) sum) (right: ('a, 'b) sum)=
((case (left, right) of
(INL l, INL l') => eql l l'
| (INR r, INR r') => eqr r r'
| _ => F
)))`;
(*let eitherEqual= eitherEqualBy (=) (=)*)
val _ = Define `
((either_setElemCompare:('d -> 'b -> ordering) ->('c -> 'a -> ordering) ->('d,'c)sum ->('b,'a)sum -> ordering) cmpa cmpb (INL x') (INL y')= (cmpa x' y'))
/\ ((either_setElemCompare:('d -> 'b -> ordering) ->('c -> 'a -> ordering) ->('d,'c)sum ->('b,'a)sum -> ordering) cmpa cmpb (INR x') (INR y')= (cmpb x' y'))
/\ ((either_setElemCompare:('d -> 'b -> ordering) ->('c -> 'a -> ordering) ->('d,'c)sum ->('b,'a)sum -> ordering) cmpa cmpb (INL _) (INR _)= LESS)
/\ ((either_setElemCompare:('d -> 'b -> ordering) ->('c -> 'a -> ordering) ->('d,'c)sum ->('b,'a)sum -> ordering) cmpa cmpb (INR _) (INL _)= GREATER)`;
(* -------------------------------------------------------------------------- *)
(* Utility functions. *)
(* -------------------------------------------------------------------------- *)
(*val isLeft : forall 'a 'b. either 'a 'b -> bool*)
(*val isRight : forall 'a 'b. either 'a 'b -> bool*)
(*val either : forall 'a 'b 'c. ('a -> 'c) -> ('b -> 'c) -> either 'a 'b -> 'c*)
(*let either fa fb x= match x with
| Left a -> fa a
| Right b -> fb b
end*)
(*val partitionEither : forall 'a 'b. list (either 'a 'b) -> (list 'a * list 'b)*)
val _ = Define `
((SUM_PARTITION:(('a,'b)sum)list -> 'a list#'b list) ([])= ([], []))
/\ ((SUM_PARTITION:(('a,'b)sum)list -> 'a list#'b list) (x :: xs)= ((
let (ll, rl) = (SUM_PARTITION xs) in
(case x of
INL l => ((l::ll), rl)
| INR r => (ll, (r::rl))
)
)))`;
(*val lefts : forall 'a 'b. list (either 'a 'b) -> list 'a*)
(*val rights : forall 'a 'b. list (either 'a 'b) -> list 'b*)
val _ = export_theory()
|
