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