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
|
chapter \<open>Generated by Lem from either.lem.\<close>
theory "Lem_either"
imports
Main
"Lem_bool"
"Lem_basic_classes"
"Lem_list"
"Lem_tuple"
begin
(*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*)
definition eitherEqualBy :: "('a \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow>('b \<Rightarrow> 'b \<Rightarrow> bool)\<Rightarrow>('a,'b)sum \<Rightarrow>('a,'b)sum \<Rightarrow> bool " where
" eitherEqualBy 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'
| _ => False
))"
(*let eitherEqual= eitherEqualBy (=) (=)*)
fun either_setElemCompare :: "('d \<Rightarrow> 'b \<Rightarrow> ordering)\<Rightarrow>('c \<Rightarrow> 'a \<Rightarrow> ordering)\<Rightarrow>('d,'c)sum \<Rightarrow>('b,'a)sum \<Rightarrow> ordering " where
" either_setElemCompare cmpa cmpb (Inl x') (Inl y') = ( cmpa x' y' )"
|" either_setElemCompare cmpa cmpb (Inr x') (Inr y') = ( cmpb x' y' )"
|" either_setElemCompare cmpa cmpb (Inl _) (Inr _) = ( LT )"
|" either_setElemCompare cmpa cmpb (Inr _) (Inl _) = ( GT )"
(* -------------------------------------------------------------------------- *)
(* 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)*)
(*let rec partitionEither l= match l with
| [] -> ([], [])
| x :: xs -> begin
let (ll, rl) = partitionEither xs in
match x with
| Left l -> (l::ll, rl)
| Right r -> (ll, r::rl)
end
end
end*)
(*val lefts : forall 'a 'b. list (either 'a 'b) -> list 'a*)
(*val rights : forall 'a 'b. list (either 'a 'b) -> list 'b*)
end
|
