Theory "fixedPoint"

Parents     pred_set

Signature

Constant Type
closed :((α -> bool) -> α -> bool) -> (α -> bool) -> bool
dense :((α -> bool) -> α -> bool) -> (α -> bool) -> bool
empty :α -> β -> bool
fnsum :(β -> α -> bool) -> (β -> α -> bool) -> β -> α -> bool
gfp :((α -> bool) -> α -> bool) -> α -> bool
lfp :((α -> bool) -> α -> bool) -> α -> bool
monotone :((α -> bool) -> β -> bool) -> bool

Definitions

monotone_def 
|- ∀f. monotone f ⇔ ∀X Y. X ⊆ Y ⇒ f X ⊆ f Y
lfp_def 
|- ∀f. lfp f = BIGINTER {X | f X ⊆ X}
gfp_def 
|- ∀f. gfp f = BIGUNION {X | X ⊆ f X}
closed_def 
|- ∀f X. closed f X ⇔ f X ⊆ X
dense_def 
|- ∀f X. dense f X ⇔ X ⊆ f X
fnsum_def 
|- ∀f1 f2 X. fnsum f1 f2 X = f1 X ∪ f2 X
empty_def 
|- empty = (λX. ∅)

Theorems

lfp_least_closed 
|- ∀f. monotone f ⇒ closed f (lfp f) ∧ ∀X. closed f X ⇒ lfp f ⊆ X
gfp_greatest_dense 
|- ∀f. monotone f ⇒ dense f (gfp f) ∧ ∀X. dense f X ⇒ X ⊆ gfp f
lfp_fixedpoint 
|- ∀f. monotone f ⇒ (lfp f = f (lfp f)) ∧ ∀X. (X = f X) ⇒ lfp f ⊆ X
gfp_greatest_fixedpoint 
|- ∀f. monotone f ⇒ (gfp f = f (gfp f)) ∧ ∀X. (X = f X) ⇒ X ⊆ gfp f
lfp_induction 
|- ∀f. monotone f ⇒ ∀X. f X ⊆ X ⇒ lfp f ⊆ X
gfp_coinduction 
|- ∀f. monotone f ⇒ ∀X. X ⊆ f X ⇒ X ⊆ gfp f
lfp_strong_induction 
|- ∀f. monotone f ⇒ ∀X. f (X ∩ lfp f) ⊆ X ⇒ lfp f ⊆ X
gfp_strong_coinduction 
|- ∀f. monotone f ⇒ ∀X. X ⊆ f (X ∪ gfp f) ⇒ X ⊆ gfp f
fnsum_monotone 
|- ∀f1 f2. monotone f1 ∧ monotone f2 ⇒ monotone (fnsum f1 f2)
empty_monotone 
|- monotone empty
fnsum_empty 
|- ∀f. (fnsum f empty = f) ∧ (fnsum empty f = f)
fnsum_ASSOC 
|- ∀f g h. fnsum f (fnsum g h) = fnsum (fnsum f g) h
fnsum_COMM 
|- ∀f g. fnsum f g = fnsum g f
fnsum_SUBSET 
|- ∀f g X. f X ⊆ fnsum f g X ∧ g X ⊆ fnsum f g X
lfp_fnsum 
|- ∀f1 f2.
     monotone f1 ∧ monotone f2 ⇒
     lfp f1 ⊆ lfp (fnsum f1 f2) ∧ lfp f2 ⊆ lfp (fnsum f1 f2)
lfp_rule_applied 
|- ∀f X y. monotone f ∧ X ⊆ lfp f ∧ y ∈ f X ⇒ y ∈ lfp f
lfp_empty 
|- ∀f x. monotone f ∧ x ∈ f ∅ ⇒ x ∈ lfp f