1 files changed, 448 insertions, 0 deletions
diff --git a/snapshots/hol4/lem/hol-lib/lem_relationScript.sml b/snapshots/hol4/lem/hol-lib/lem_relationScript.sml
new file mode 100644
index 00000000..e73b66ce
--- /dev/null
+++ b/snapshots/hol4/lem/hol-lib/lem_relationScript.sml
@@ -0,0 +1,448 @@
+(*Generated by Lem from relation.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_tupleTheory lem_setTheory lem_numTheory set_relationTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_relation"
+
+
+
+(*open import Bool Basic_classes Tuple Set Num*)
+(*open import {hol} `set_relationTheory`*)
+
+(* ========================================================================== *)
+(* The type of relations                                                      *)
+(* ========================================================================== *)
+
+val _ = type_abbrev((* ( 'a, 'b) *) "rel_pred" , ``: 'a -> 'b -> bool``);
+val _ = type_abbrev((* ( 'a, 'b) *) "rel_set" , ``: ('a # 'b) set``);
+
+(* Binary relations are usually represented as either
+   sets of pairs (rel_set) or as curried functions (rel_pred). 
+   
+   The choice depends on taste and the backend. Lem should not take a 
+   decision, but supports both representations. There is an abstract type
+   pred, which can be converted to both representations. The representation
+   of pred itself then depends on the backend. However, for the time beeing,
+   let's implement relations as sets to get them working more quickly. *)
+
+val _ = type_abbrev((* ( 'a, 'b) *) "rel" , ``: ('a, 'b) rel_set``);
+
+(*val relToSet : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel_set 'a 'b*)
+(*val relFromSet : forall 'a 'b. SetType 'a, SetType 'b => rel_set 'a 'b -> rel 'a 'b*)
+
+(*val relEq : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel 'a 'b -> bool*)
+val _ = Define `
+ ((relEq:('a#'b)set ->('a#'b)set -> bool) r1 r2=  (r1 = r2))`;
+
+
+(*val relToPred : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> rel_pred 'a 'b*)
+(*val relFromPred : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => set 'a -> set 'b -> rel_pred 'a 'b -> rel 'a 'b*)
+
+(*let relToPred r=  (fun x y -> (x, y) IN relToSet r)*)
+val _ = Define `
+ ((relFromPred:'a set -> 'b set ->('a -> 'b -> bool) ->('a#'b)set) xs ys p=  (SET_FILTER (\ (x,y) .  p x y) (xs CROSS ys)))`;
+
+
+ 
+(* ========================================================================== *)
+(* Basic Operations                                                           *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* membership test         *)
+(* ----------------------- *)
+
+(*val inRel : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => 'a -> 'b -> rel 'a 'b -> bool*)
+
+
+(* ----------------------- *)
+(* empty relation          *)
+(* ----------------------- *)
+
+(*val relEmpty : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b*)
+
+(* ----------------------- *)
+(* Insertion               *)
+(* ----------------------- *)
+
+(*val relAdd : forall 'a 'b. SetType 'a, SetType 'b => 'a -> 'b -> rel 'a 'b -> rel 'a 'b*)
+
+
+(* ----------------------- *)
+(* Identity relation       *)
+(* ----------------------- *)
+
+(*val relIdOn : forall 'a. SetType 'a, Eq 'a => set 'a -> rel 'a 'a*)
+val _ = Define `
+ ((relIdOn:'a set ->('a#'a)set) s=  (relFromPred s s (=)))`;
+
+
+(*val relId : forall 'a. SetType 'a, Eq 'a => rel 'a 'a*)
+val _ = Define `
+ ((relId:('a#'a)set)=  ({(x, x) |  x | T}))`;
+
+
+(* ----------------------- *)
+(* relation union          *)
+(* ----------------------- *)
+
+(*val relUnion : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel 'a 'b -> rel 'a 'b*) 
+
+(* ----------------------- *)
+(* relation intersection   *)
+(* ----------------------- *)
+
+(*val relIntersection : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> rel 'a 'b -> rel 'a 'b*) 
+
+(* ----------------------- *)
+(* Relation Composition    *)
+(* ----------------------- *)
+
+(*val relComp : forall 'a 'b 'c. SetType 'a, SetType 'b, SetType 'c, Eq 'a, Eq 'b => rel 'a 'b -> rel 'b 'c -> rel 'a 'c*)
+(*let relComp r1 r2=  relFromSet {(e1, e3) | forall ((e1,e2) IN (relToSet r1)) ((e2',e3) IN (relToSet r2)) | e2 = e2'}*)
+
+(* ----------------------- *)
+(* restrict                *)
+(* ----------------------- *)
+
+(*val relRestrict : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> rel 'a 'a*)
+(*let relRestrict r s=  relFromSet ({ (a, b) | forall (a IN s) (b IN s) | inRel a b r })*)
+
+
+(* ----------------------- *)
+(* Converse                *)
+(* ----------------------- *)
+
+(*val relConverse : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel 'b 'a*)
+val _ = Define `
+ ((lem_converse:('a#'b)set ->('b#'a)set) r=  (IMAGE SWAP (r)))`;
+
+
+
+(* ----------------------- *)
+(* domain                  *)
+(* ----------------------- *)
+
+(*val relDomain : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> set 'a*)
+(*let relDomain r=  Set.map (fun x -> fst x) (relToSet r)*)
+
+(* ----------------------- *)
+(* range                   *)
+(* ----------------------- *)
+
+(*val relRange : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> set 'b*)
+(*let relRange r=  Set.map (fun x -> snd x) (relToSet r)*)
+
+
+(* ----------------------- *)
+(* field / definedOn       *)
+(*                         *)
+(* avoid the keyword field *)
+(* ----------------------- *)
+
+(*val relDefinedOn : forall 'a. SetType 'a => rel 'a 'a -> set 'a*)
+
+(* ----------------------- *)
+(* relOver                 *)
+(*                         *)
+(* avoid the keyword field *)
+(* ----------------------- *)
+
+(*val relOver : forall 'a. SetType 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((rel_over:('a#'a)set -> 'a set -> bool) r s=  ((((domain r) UNION (range r))) SUBSET s))`;
+
+
+
+(* ----------------------- *)
+(* apply a relation        *)
+(* ----------------------- *)
+
+(* Given a relation r and a set s, relApply r s applies s to r, i.e.
+   it returns the set of all value reachable via r from a value in s.
+   This operation can be seen as a generalisation of function application. *)
+   
+(*val relApply : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a => rel 'a 'b -> set 'a -> set 'b*)
+val _ = Define `
+ ((rapply:('a#'b)set -> 'a set -> 'b set) r s= 
+  ({ y | x, y | ((x, y) IN (r)) /\ (x IN s) }))`;
+
+
+
+(* ========================================================================== *)
+(* Properties                                                                 *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* subrel                  *)
+(* ----------------------- *)
+
+(*val isSubrel : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> rel 'a 'b -> bool*)
+
+(* ----------------------- *)
+(* reflexivity             *)
+(* ----------------------- *)
+
+(*val isReflexiveOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_reflexive_on:('a#'a)set -> 'a set -> bool) r s=  (! (e :: s). (e, e) IN r))`;
+
+
+(*val isReflexive : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_reflexive:('a#'a)set -> bool) r=  (! e. (e, e) IN r))`;
+
+
+
+(* ----------------------- *)
+(* irreflexivity           *)
+(* ----------------------- *)
+
+(*val isIrreflexiveOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+(*let isIrreflexiveOn r s=  (forall (e IN s). not (inRel e e r))*)
+
+(*val isIrreflexive : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_irreflexive:('a#'a)set -> bool) r=  (! ((e1, e2) :: (r)). ~ (e1 = e2)))`;
+
+
+
+(* ----------------------- *)
+(* symmetry                *)
+(* ----------------------- *)
+
+(*val isSymmetricOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_symmetric_on:('a#'a)set -> 'a set -> bool) r s=  (! (e1 :: s) (e2 :: s). ((e1, e2) IN r) ==> ((e2, e1) IN r)))`;
+
+
+(*val isSymmetric : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_symmetric:('a#'a)set -> bool) r=  (! ((e1, e2) :: r). (e2, e1) IN r))`;
+
+
+
+(* ----------------------- *)
+(* antisymmetry            *)
+(* ----------------------- *)
+
+(*val isAntisymmetricOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_antisymmetric_on:('a#'a)set -> 'a set -> bool) r s=  (! (e1 :: s) (e2 :: s). ((e1, e2) IN r) ==> (((e2, e1) IN r) ==> (e1 = e2))))`;
+
+
+(*val isAntisymmetric : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+(*let isAntisymmetric r=  (forall ((e1, e2) IN relToSet r). (inRel e2 e1 r) --> (e1 = e2))*)
+
+
+(* ----------------------- *)
+(* transitivity            *)
+(* ----------------------- *)
+
+(*val isTransitiveOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_transitive_on:('a#'a)set -> 'a set -> bool) r s=  (! (e1 :: s) (e2 :: s) (e3 :: s). ((e1, e2) IN r) ==> (((e2, e3) IN r) ==> ((e1, e3) IN r))))`;
+
+
+(*val isTransitive : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+(*let isTransitive r=  (forall ((e1, e2) IN relToSet r) (e3 IN relApply r {e2}). inRel e1 e3 r)*)
+
+(* ----------------------- *)
+(* total                   *)
+(* ----------------------- *)
+
+(*val isTotalOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_total_on:('a#'a)set -> 'a set -> bool) r s=  (! (e1 :: s) (e2 :: s). ((e1, e2) IN r) \/ ((e2, e1) IN r)))`;
+
+
+
+(*val isTotal : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_total:('a#'a)set -> bool) r=  (! e1 e2. ((e1, e2) IN r) \/ ((e2, e1) IN r)))`;
+
+
+(*val isTrichotomousOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_trichotomous_on:('a#'a)set -> 'a set -> bool) r s=  (! (e1 :: s) (e2 :: s). ((e1, e2) IN r) \/ ((e1 = e2) \/ ((e2, e1) IN r))))`;
+
+
+(*val isTrichotomous : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_trichotomous:('a#'a)set -> bool) r=  (! e1 e2. ((e1, e2) IN r) \/ ((e1 = e2) \/ ((e2, e1) IN r))))`;
+
+
+
+(* ----------------------- *)
+(* is_single_valued        *)
+(* ----------------------- *)
+
+(*val isSingleValued : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> bool*)
+val _ = Define `
+ ((lem_is_single_valued:('a#'b)set -> bool) r=  (! ((e1, e2a) :: r) (e2b :: rapply r {e1}). e2a = e2b))`;
+
+
+
+(* ----------------------- *)
+(* equivalence relation    *)
+(* ----------------------- *)
+
+(*val isEquivalenceOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_equivalence_on:('a#'a)set -> 'a set -> bool) r s=  (lem_is_reflexive_on r s /\ lem_is_symmetric_on r s /\ lem_transitive_on r s))`;
+
+
+
+(*val isEquivalence : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_equivalence:('a#'a)set -> bool) r=  (lem_is_reflexive r /\ lem_is_symmetric r /\ transitive r))`;
+
+
+
+(* ----------------------- *)
+(* well founded            *)
+(* ----------------------- *)
+
+(*val isWellFounded : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+(*let ~{ocaml;coq} isWellFounded r=  (forall P. (forall x. (forall y. inRel y x r --> P x) --> P x) --> (forall x. P x))*)
+
+
+(* ========================================================================== *)
+(* Orders                                                                     *)
+(* ========================================================================== *)
+
+
+(* ----------------------- *)
+(* pre- or quasiorders     *)
+(* ----------------------- *)
+
+(*val isPreorderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_preorder_on:('a#'a)set -> 'a set -> bool) r s=  (lem_is_reflexive_on r s /\ lem_transitive_on r s))`;
+
+
+(*val isPreorder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_preorder:('a#'a)set -> bool) r=  (lem_is_reflexive r /\ transitive r))`;
+
+
+
+(* ----------------------- *)
+(* partial orders          *)
+(* ----------------------- *)
+
+(*val isPartialOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_partial_order_on:('a#'a)set -> 'a set -> bool) r s=  (lem_is_reflexive_on r s /\ lem_transitive_on r s /\ lem_is_antisymmetric_on r s))`;
+
+
+
+(*val isStrictPartialOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_strict_partial_order_on:('a#'a)set -> 'a set -> bool) r s=  (irreflexive r s /\ lem_transitive_on r s))`;
+
+
+
+(*val isStrictPartialOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_strict_partial_order:('a#'a)set -> bool) r=  (lem_is_irreflexive r /\ transitive r))`;
+
+
+(*val isPartialOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_partial_order:('a#'a)set -> bool) r=  (lem_is_reflexive r /\ transitive r /\ antisym r))`;
+
+
+(* ----------------------- *)
+(* total / linear orders   *)
+(* ----------------------- *)
+
+(*val isTotalOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_total_order_on:('a#'a)set -> 'a set -> bool) r s=  (lem_is_partial_order_on r s /\ lem_is_total_on r s))`;
+
+
+(*val isStrictTotalOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+val _ = Define `
+ ((lem_is_strict_total_order_on:('a#'a)set -> 'a set -> bool) r s=  (lem_is_strict_partial_order_on r s /\ lem_is_trichotomous_on r s))`;
+
+
+(*val isTotalOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_total_order:('a#'a)set -> bool) r=  (lem_is_partial_order r /\ lem_is_total r))`;
+
+
+(*val isStrictTotalOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+val _ = Define `
+ ((lem_is_strict_total_order:('a#'a)set -> bool) r=  (lem_is_strict_partial_order r /\ lem_is_trichotomous r))`;
+
+
+
+
+(* ========================================================================== *)
+(* closures                                                                   *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* transitive closure      *)
+(* ----------------------- *)
+
+(*val transitiveClosure : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*)
+(*val transitiveClosureByEq  : forall 'a. ('a -> 'a -> bool) -> rel 'a 'a -> rel 'a 'a*)
+(*val transitiveClosureByCmp : forall 'a. ('a * 'a -> 'a * 'a -> Basic_classes.ordering) -> rel 'a 'a -> rel 'a 'a*)
+
+
+(* ----------------------- *)
+(* transitive closure step *)
+(* ----------------------- *)
+
+(*val transitiveClosureAdd : forall 'a. SetType 'a, Eq 'a => 'a -> 'a -> rel 'a 'a -> rel 'a 'a*)
+
+val _ = Define `
+ ((tc_insert:'a -> 'a ->('a#'a)set ->('a#'a)set) x y r=  
+  ((((((x,y) INSERT (r)))) UNION ((((({(x, z) | z | 
+  (z IN range r) /\ ((y, z) IN r)})) UNION (({(z, y) | z | 
+  (z IN domain r) /\ ((z, x) IN r)}))))))))`;
+
+
+
+(* ========================================================================== *)
+(* reflexive closure                                                          *)
+(* ========================================================================== *)
+
+(*val reflexiveTransitiveClosureOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> rel 'a 'a*)
+val _ = Define `
+ ((reflexive_transitive_closure_on:('a#'a)set -> 'a set ->('a#'a)set) r s=  (tc (((r) UNION ((relIdOn s))))))`;
+
+
+
+(*val reflexiveTransitiveClosure : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*)
+val _ = Define `
+ ((reflexiveTransitiveClosure:('a#'a)set ->('a#'a)set) r=  (tc (((r) UNION (relId)))))`;
+
+
+
+
+(* ========================================================================== *)
+(* inverse of closures                                                        *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* without transitve edges *)
+(* ----------------------- *)
+
+(*val withoutTransitiveEdges: forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*)
+val _ = Define `
+ ((withoutTransitiveEdges:('a#'a)set ->('a#'a)set) r=  
+ (let tc1 = (tc r) in
+  {(a, c) | a, c 
+  | ((a, c) IN r) /\
+   (! (b :: range r).
+      ((a <> b) /\ (b <> c)) ==> ~ (((a, b) IN tc1) /\ ((b, c) IN tc1)))}))`;
+
+val _ = export_theory()
+