-- 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
Intros
Unfold MakePER
Intros
Apply H1
Assumption
Exit

prove MakePER_sym : @Y:*s. @R:Y->Y->*p. @y1,y2:Y. 
                          MakePER R y1 y2 -> MakePER R y2 y1
Intros
Unfold MakePER
Intros
Unfold IsPER In H2
AndE H2
Apply H3
Apply H Then Assumption
Exit


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
Intros
Unfold MakePER
Intros
Unfold IsPER In H3
AndE H3
Apply H5 On y2
Apply H Then Assumption
Apply H1 Then Assumption
Exit

Prove MakePER_PER : @Y:*s.@R:Y->Y->*p. IsPER (MakePER R)
Intros
Unfold IsPER
AndI
Apply MakePER_sym
Apply MakePER_trans
Exit


Prove IsPER_closed_function : @A,B:*s.@f:A->B.@(~):B->B->*p.
                              IsPER (~) -> IsPER (\a1,a2:A. f a1 ~ f a2)
Intros
Unfold IsPER In H
AndE H
Unfold IsPER
AndI
Intros 2
Apply H1
Intros 3
Apply H2
Exit





prove IsER__IsPER : @Y:*s. @R:Y->Y->*p. IsER R -> IsPER R
Intros
Unfold IsER In H
AndE H
Assumption
Exit


prove IsER_is : @A:*s. IsER ((=) A)
Intro
Unfold IsER
Repeat AndI
Apply is_refl
Apply is_sym
Apply is_trans
Exit




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
Intros
Unfold MakeER
Intros
Apply H1
Assumption
Exit

prove MakeER_refl : @Y:*s. @R:Y->Y->*p. @y:Y. MakeER R y y
Intros
Unfold MakeER
Intros
Unfold IsER In H1
AndE H1
Apply H2
Exit


prove MakeER_sym : @Y:*s. @R:Y->Y->*p. @y1,y2:Y. 
                          MakeER R y1 y2 -> MakeER R y2 y1
Intros
Unfold MakeER
Intros
Unfold IsER In H2
AndE H2
AndE H4
Apply H5
Apply H Then Assumption
Exit

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
Intros
Unfold MakeER
Intros
Unfold IsER In H3 Then AndE H3
AndE H5
Apply H7 On y2
Apply H Then Assumption
Apply H1 Then Assumption
Exit




Prove rel_LeftC : @A,B:*s. @(~):A->B->*p. 
                  @a1,a2:A.@b:B. a1~b -> a2~b -> LeftC (~) a1 a2
Intros
Unfold LeftC
ExistsI b
AndI Then Assumption
Exit



prove LeftC_sym : @Y,Z:*s. @(~):Y->Z->*p. @y1,y2:Y. LeftC (~) y1 y2 ->
                                                    LeftC (~) y2 y1
Unfold LeftC
Intros
ExistsE H
ExistsI z
Apply And_sym
Assumption
Exit

Prove LeftC_trans : @A,B:*s. @(~):A->B->*p. IsZclosed (~) ->
                    @x,y,z:A. LeftC (~) x y -> LeftC (~) y z -> LeftC (~) x z
Unfold LeftC
Intros
ExistsE H1
ExistsE H2
AndE H3
AndE H4
ExistsI z1
AndI
Assumption
Apply H On H7 Then Assumption
Exit

prove LeftC_semirefl : @Y,Z:*s. @(~):Y->Z->*p. @y1,y2:Y. LeftC (~) y1 y2 ->
                                                    LeftC (~) y1 y1
Intros
Unfold LeftC In H
ExistsE H
Unfold LeftC
ExistsI z
AndE H1
AndI Then Assumption
Exit


Prove rel_RightC : @A,B:*s. @(~):A->B->*p. 
                  @a:A.@b1,b2:B. a~b1 -> a~b2 -> RightC (~) b1 b2
Intros
Unfold RightC
ExistsI a
AndI Then Assumption
Exit

prove IsZclosed__IsPER_LeftC : @Y,Z:*s. @R:Y->Z->*p.
                    IsZclosed R -> IsPER (LeftC R)
Intros
Unfold IsZclosed In H
Unfold IsPER
AndI
Intros
Unfold LeftC In H1
ExistsE H1
Unfold LeftC
ExistsI z
Apply And_sym
Assumption
Intros
Unfold LeftC In H1
ExistsE H1
Unfold LeftC In H2
ExistsE H2
Unfold LeftC
ExistsI z
AndE H3
AndE H4
AndI
Assumption
Apply H On H7 Then Assumption
Exit



prove IsZclosed__IsPER_RightC : @Y,Z:*s. @R:Y->Z->*p.
                    IsZclosed R -> IsPER (RightC R)
Intros
Unfold IsZclosed In H
Unfold IsPER
AndI
Intros
Unfold RightC In H1
ExistsE H1
Unfold RightC
ExistsI y
Apply And_sym
Assumption
Intros
Unfold RightC In H1
ExistsE H1
Unfold RightC In H2
ExistsE H2
Unfold RightC
ExistsI y
AndE H3
AndE H4
AndI
Assumption
Apply H On H7 Then Assumption
Exit

                  
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
Intros
Unfold MakeZclosed
Intros
Apply H1
Assumption
Exit

prove MakeZclosed_Zclosed : @Y,Z:*s. @R:Y->Z->*p.
                            IsZclosed (MakeZclosed R)
Intros
Unfold IsZclosed
Intros
Unfold MakeZclosed
Intros
Unfold IsZclosed In H4
Apply H4 On y1, z2
Apply H Then Assumption
Apply H1 Then Assumption
Apply H2 Then Assumption
Exit


Prove IsERon_is : @A:*s. @P:A->*p. IsERon ((=) A) P
Intros
Apply IsER__IsERon
Apply IsER_is
Exit


-- 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
Intros
Apply equiv_predR
Unfold Inverse
Intros
Refl
Exit



-- 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)
Intros
Unfold IsERon In H
AndE H
AndE H2
Unfold IsER
AndI
Intro
Apply H1
Apply Image_f_f_x
AndI
Intros 2
Apply H3
Apply Image_f_f_x
Apply Image_f_f_x
Intros 3
Apply H4
Apply Image_f_f_x
Apply Image_f_f_x
Apply Image_f_f_x
Exit

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
Intros
Unfold IsERon In H
AndE H
AndE H2
Unfold IsERon
Repeat AndI
Intros
Repeat AndI Then Try Assumption
Apply H1 Then Assumption
Intros
AndE H7
AndE H9
Repeat AndI Then Try Apply H3 Then Assumption
Intros
Repeat AndI
Assumption
AndE H8
AndE H11
AndE H9
AndE H15
Apply H4 On H16 Then Try Assumption
AndE H9
AndE H11
Assumption
Exit


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

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

prove IsZclosed_Inverse :  @A,B:*s.@(~):A->B->*p.
                           IsZclosed (~) -> IsZclosed (Inverse (~))
Unfold Inverse
Unfold IsZclosed
Intros 8
Intros
Apply H On H2
Assumption
Assumption
Exit


Prove IsERon_Dom : @A:*s. @(~):A->A->*p. IsPER (~) ->
                   IsERon (~) (Dom (~))
Intros
Unfold IsPER In H
AndE H
Unfold IsERon
Repeat AndI
Unfold Dom
Intros
ExistsE H3
Apply H2 On H4
Apply H1
Assumption
Intros
Apply H1
Assumption
Intros
Apply H2 On H6, H7
Exit