-- 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