1 files changed, 83 insertions, 0 deletions
diff --git a/prover_snapshots/hol4/lib/lem/lem_eitherScript.sml b/prover_snapshots/hol4/lib/lem/lem_eitherScript.sml
new file mode 100644
index 0000000..cad5388
--- /dev/null
+++ b/prover_snapshots/hol4/lib/lem/lem_eitherScript.sml
@@ -0,0 +1,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()
+