Theory: relation

Parents

• combin

Types

Constants

• the_fun  :('a -> 'a -> bool) -> (('a -> 'b) -> 'a -> 'b) -> 'a -> 'a -> 'b
• RESTRICT  :('a -> 'b) -> ('a -> 'a -> bool) -> 'a -> 'a -> 'b
• TC  :('a -> 'a -> bool) -> 'a -> 'a -> bool
• WF  :('a -> 'a -> bool) -> bool
• WFREC  :('a -> 'a -> bool) -> (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b
• inv_image  :('b -> 'b -> bool) -> ('a -> 'b) -> 'a -> 'a -> bool
• Empty  :'a -> 'a -> bool
• approx  :('a -> 'a -> bool) -> (('a -> 'b) -> 'a -> 'b) -> 'a -> ('a -> 'b) -> bool
• transitive  :('a -> 'a -> bool) -> bool

Definitions

approx_def

|- !R M x f. approx R M x f = (f = RESTRICT (\y. M (RESTRICT f R y) y) R x)

Empty_def

|- !x y. Empty x y = F

inv_image_def

|- !R f. inv_image R f = (\x y. R (f x) (f y))

RESTRICT_DEF

|- !f R x. RESTRICT f R x = (\y. (if R y x then f y else ARB))

TC_DEF

|- !R a b.
     TC R a b =
     !P.
       (!x y. R x y ==> P x y) /\ (!x y z. P x y /\ P y z ==> P x z) ==> P a b

the_fun_def

|- !R M x. the_fun R M x = @f. approx R M x f

transitive_def

|- !R. transitive R = !x y z. R x y /\ R y z ==> R x z

WF_DEF

|- !R. WF R = !B. (?w. B w) ==> ?min. B min /\ !b. R b min ==> ~B b

WFREC_DEF

|- !R M.
     WFREC R M =
     (\x. M (RESTRICT (the_fun (TC R) (\f v. M (RESTRICT f R v) v) x) R x) x)

Theorems

RESTRICT_LEMMA

|- !f R y z. R y z ==> (RESTRICT f R z y = f y)

TC_CASES1

|- !R x z. TC R x z ==> R x z \/ ?y. R x y /\ TC R y z

TC_CASES2

|- !R x z. TC R x z ==> R x z \/ ?y. TC R x y /\ R y z

TC_INDUCT

|- !R P.
     (!x y. R x y ==> P x y) /\ (!x y z. P x y /\ P y z ==> P x z) ==>
     !u v. TC R u v ==> P u v

TC_SUBSET

|- !R x y. R x y ==> TC R x y

TC_TRANSITIVE

|- !R. transitive (TC R)

WF_Empty

|- WF Empty

WF_INDUCTION_THM

|- !R. WF R ==> !P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. P x

WF_inv_image

|- !R f. WF R ==> WF (inv_image R f)

WF_NOT_REFL

|- !R x y. WF R ==> R x y ==> ~(x = y)

WF_RECURSION_THM

|- !R. WF R ==> !M. ?!f. !x. f x = M (RESTRICT f R x) x

WF_SUBSET

|- !R P. WF R /\ (!x y. P x y ==> R x y) ==> WF P

WF_TC

|- !R. WF R ==> WF (TC R)

WFREC_COROLLARY

|- !M R f. (f = WFREC R M) ==> WF R ==> !x. f x = M (RESTRICT f R x) x

WFREC_THM

|- !R M. WF R ==> !x. WFREC R M x = M (RESTRICT (WFREC R M) R x) x