Theory "fixedPoint"

Parents     pred_set   poset

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

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

Theorems

SUBSET_complete 
⊢ complete (𝕌(:α -> bool),$SUBSET)
SUBSET_poset 
⊢ poset (𝕌(:α -> bool),$SUBSET)
empty_monotone 
⊢ monotone empty
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
fnsum_empty 
⊢ ∀f. (fnsum f empty = f) ∧ (fnsum empty f = f)
fnsum_monotone 
⊢ ∀f1 f2. monotone f1 ∧ monotone f2 ⇒ monotone (fnsum f1 f2)
gfp_coinduction 
⊢ ∀f. monotone f ⇒ ∀X. X ⊆ f X ⇒ X ⊆ gfp f
gfp_greatest_dense 
⊢ ∀f. monotone f ⇒ dense f (gfp f) ∧ ∀X. dense f X ⇒ X ⊆ gfp f
gfp_greatest_fixedpoint 
⊢ ∀f. monotone f ⇒ (f (gfp f) = gfp f) ∧ ∀X. (f X = X) ⇒ X ⊆ gfp f
gfp_poset_gfp 
⊢ monotone f ⇒ po_gfp (𝕌(:α -> bool),$SUBSET) f (gfp f)
gfp_strong_coinduction 
⊢ ∀f. monotone f ⇒ ∀X. X ⊆ f (X ∪ gfp f) ⇒ X ⊆ gfp f
lfp_empty 
⊢ ∀f x. monotone f ∧ x ∈ f ∅ ⇒ x ∈ lfp f
lfp_fixedpoint 
⊢ ∀f. monotone f ⇒ (f (lfp f) = lfp f) ∧ ∀X. (f X = X) ⇒ lfp f ⊆ X
lfp_fnsum 
⊢ ∀f1 f2.
    monotone f1 ∧ monotone f2 ⇒
    lfp f1 ⊆ lfp (fnsum f1 f2) ∧ lfp f2 ⊆ lfp (fnsum f1 f2)
lfp_induction 
⊢ ∀f. monotone f ⇒ ∀X. f X ⊆ X ⇒ lfp f ⊆ X
lfp_least_closed 
⊢ ∀f. monotone f ⇒ closed f (lfp f) ∧ ∀X. closed f X ⇒ lfp f ⊆ X
lfp_poset_lfp 
⊢ monotone f ⇒ po_lfp (𝕌(:α -> bool),$SUBSET) f (lfp f)
lfp_rule_applied 
⊢ ∀f X y. monotone f ∧ X ⊆ lfp f ∧ y ∈ f X ⇒ y ∈ lfp f
lfp_strong_induction 
⊢ ∀f. monotone f ⇒ ∀X. f (X ∩ lfp f) ⊆ X ⇒ lfp f ⊆ X
monotonic_monotone 
⊢ monotonic (𝕌(:α -> bool),$SUBSET) f ⇔ monotone f