Theory Lem_either

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