-- File: prelimsOver
-- hoort niet in cleaned up versie thuis.


-- Wat feitjes over bisimulatie-relaties e.d.
-- 1. De reflexieve, symmetrische en transitieve afsluiting is weer een
--    bisimulatie-relatie.

Path "../lol"
Read "lambdaL"
Load "logic2"


def IsPER := \Y:*s. \R:Y->Y->*p.
                    (@y1,y2:Y. R y1 y2 -> R y2 y1) /\
                    (@y1,y2,y3:Y. R y1 y2 -> R y2 y3 -> R y1 y3)
implicit 1 IsPER

def MakePER := \Y:*s. \R:Y->Y->*p. \y1,y2:Y.
                   @E:Y->Y->*p.
                       (@z1,z2:Y. R z1 z2 -> E z1 z2) ->
                       IsPER E ->
                       E y1 y2 :
              @Y:*s. (Y->Y->*p) -> (Y->Y->*p)
implicit 1 MakePER
              
prove MakePER_ext : @Y:*s. @R:Y->Y->*p. @y1,y2:Y. R y1 y2 -> MakePER R y1 y2

prove MakePER_sym : @Y:*s. @R:Y->Y->*p. @y1,y2:Y. 
                          MakePER R y1 y2 -> MakePER R y2 y1


prove MakePER_trans : @Y:*s. @R:Y->Y->*p. @y1,y2,y3:Y. 
                       MakePER R y1 y2 ->  MakePER R y2 y3 -> MakePER R y1 y3

Prove MakePER_PER : @Y:*s.@R:Y->Y->*p. IsPER (MakePER R)


Prove IsPER_closed_function : @A,B:*s.@f:A->B.@(~):B->B->*p.
                              IsPER (~) -> IsPER (\a1,a2:A. f a1 ~ f a2)





prove IsER__IsPER : @Y:*s. @R:Y->Y->*p. IsER R -> IsPER R


prove IsER_is : @A:*s. IsER ((=) A)




def MakeER := \Y:*s. \R:Y->Y->*p. \y1,y2:Y.
                   @E:Y->Y->*p.
                       (@z1,z2:Y. R z1 z2 -> E z1 z2) ->
                       IsER E ->
                       E y1 y2 :
              @Y:*s. (Y->Y->*p) -> (Y->Y->*p)
implicit 1 MakeER

prove MakeER_ext : @Y:*s. @R:Y->Y->*p. @y1,y2:Y. R y1 y2 -> MakeER R y1 y2

prove MakeER_refl : @Y:*s. @R:Y->Y->*p. @y:Y. MakeER R y y


prove MakeER_sym : @Y:*s. @R:Y->Y->*p. @y1,y2:Y. 
                          MakeER R y1 y2 -> MakeER R y2 y1

prove MakeER_trans : @Y:*s. @R:Y->Y->*p. @y1,y2,y3:Y. 
                       MakeER R y1 y2 ->  MakeER R y2 y3 -> MakeER R y1 y3




Prove rel_LeftC : @A,B:*s. @(~):A->B->*p. 
                  @a1,a2:A.@b:B. a1~b -> a2~b -> LeftC (~) a1 a2



prove LeftC_sym : @Y,Z:*s. @(~):Y->Z->*p. @y1,y2:Y. LeftC (~) y1 y2 ->
                                                    LeftC (~) y2 y1

Prove LeftC_trans : @A,B:*s. @(~):A->B->*p. IsZclosed (~) ->
                    @x,y,z:A. LeftC (~) x y -> LeftC (~) y z -> LeftC (~) x z

prove LeftC_semirefl : @Y,Z:*s. @(~):Y->Z->*p. @y1,y2:Y. LeftC (~) y1 y2 ->
                                                    LeftC (~) y1 y1


Prove rel_RightC : @A,B:*s. @(~):A->B->*p. 
                  @a:A.@b1,b2:B. a~b1 -> a~b2 -> RightC (~) b1 b2

prove IsZclosed__IsPER_LeftC : @Y,Z:*s. @R:Y->Z->*p.
                    IsZclosed R -> IsPER (LeftC R)



prove IsZclosed__IsPER_RightC : @Y,Z:*s. @R:Y->Z->*p.
                    IsZclosed R -> IsPER (RightC R)

                  
def MakeZclosed := \Y,Z:*s. \R:Y->Z->*p. \y:Y.\z:Z.
                     @sim:Y->Z->*p.
                        (@y1:Y.@z1:Z. R y1 z1 -> sim y1 z1) ->
                        IsZclosed sim ->
                        sim y z :
                  @Y,Z:*s. (Y->Z->*p) -> (Y->Z->*p)
implicit 2 MakeZclosed

prove MakeZclosed_ext : @Y,Z:*s. @R:Y->Z->*p.
                          @y:Y.@z:Z. R y z -> MakeZclosed R y z

prove MakeZclosed_Zclosed : @Y,Z:*s. @R:Y->Z->*p.
                            IsZclosed (MakeZclosed R)


Prove IsERon_is : @A:*s. @P:A->*p. IsERon ((=) A) P


-- deelverzameling
Def (==>) := \A:*s. \P,Q:A->*p. @x:A. P x -> Q x :
              @A:*s. (A->*p) -> (A->*p) -> *p
Implicit 1 (==>)

Prove Inverse_Inverse : @A,B:*s. @R:A->B->*p. Inverse (Inverse R) <===> R



-- Deelrelatie
Def (===>) := \A,B:*s. \P,Q:A->B->*p. @x:A.@y:B. P x y -> Q x y :
              @A,B:*s. (A->B->*p) -> (A->B->*p) -> *p
Implicit 2 (===>)


Def Range := \A,B:*s. \P:A->B->*p. \b:B. Ex a:A. P a b :
             @A,B:*s. (A->B->*p) -> B->*p
Implicit 2 Range


Prove IsER_fun_rel : @A,B : *s. @f : B->A. @(~):A->A->*p.
                     IsERon (~) (Image f) ->
                     IsER (\b1,b2:B. f b1 ~ f b2)

Prove IsERon_Dom_restr : @A:*s. @(~):A->A->*p. @P:A->*p.
                         IsERon (~) P -> IsERon (\y,z:A. P y /\ y~z /\ P z) P


prove LeftC_Inverse : @A,B:*s.@(~):A->B->*p.
                      LeftC (Inverse (~)) <===> RightC (~)

prove RightC_Inverse : @A,B:*s.@(~):A->B->*p.
                      RightC (Inverse (~)) <===> LeftC (~)

prove IsZclosed_Inverse :  @A,B:*s.@(~):A->B->*p.
                           IsZclosed (~) -> IsZclosed (Inverse (~))


Prove IsERon_Dom : @A:*s. @(~):A->A->*p. IsPER (~) ->
                   IsERon (~) (Dom (~))