chapter ‹Generated by Lem from ‹either.lem›.› 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 ⇒ 'a ⇒ bool)⇒('b ⇒ 'b ⇒ bool)⇒('a,'b)sum ⇒('a,'b)sum ⇒ 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 ⇒ 'b ⇒ ordering)⇒('c ⇒ 'a ⇒ ordering)⇒('d,'c)sum ⇒('b,'a)sum ⇒ 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