(*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()