Commit 630a79b2 authored by Max Rapp's avatar Max Rapp

Add fixpoints, min/max

parent 1bcea039
......@@ -32,7 +32,12 @@ theory LeastMost : base:?Logic =
prop_isLeast : {A : type} A ⟶ (A ⟶ bool) ⟶ (A ⟶ A ⟶ bool) ⟶ bool ❘ = [A,x,P,R] P x ∧ ∀[y] P y ⇒ R x y ❘ # isLeast 2 3 4 ❙
least : {A : type} (A ⟶ bool) ⟶ (A ⟶ A ⟶ bool) ⟶ A ❘ = [A,P,R] ι [x] isLeast x P R ❘ # least 2 3❙
prop_isGreatest : {A : type} A ⟶ (A ⟶ bool) ⟶ (A ⟶ A ⟶ bool) ⟶ bool ❘ = [A,x,P,R] isLeast x P (converse R) ❘ # isGreatest 2 3 4 ❙
greatest : {A : type} (A ⟶ bool) ⟶ (A ⟶ A ⟶ bool) ⟶ A ❘ = [A,P,R] ι [x] isGreatest x P R ❘ # greatest 2 3❙
greatest : {A : type} (A ⟶ bool) ⟶ (A ⟶ A ⟶ bool) ⟶ A ❘ = [A,P,R] ι [x] isGreatest x P R ❘ # greatest 2 3❙
// least/greatest assume that there is a unique least element. Instead minimal/maximal return a set of minimal elements (a singleton
// if there is a unique one). ❙
minimal: {A : type} (A ⟶ bool) ⟶ (A ⟶ A ⟶ bool) ⟶ set A ❘ = [A,P,R] ι [s] ∀[x] x ∈ s ⇒ isLeast x P R ❘ # minimal 2 3❙
maximal: {A : type} (A ⟶ bool) ⟶ (A ⟶ A ⟶ bool) ⟶ set A ❘ = [A,P,R] ι [s] ∀[x] x ∈ s ⇒ isGreatest x P R ❘ # maximal 2 3❙
theory DirectedSet : base:?Logic =
......@@ -58,6 +63,12 @@ theory DirectedSet : base:?Logic =
directedSet = Mod directedSet_theory ❘ role abbreviation ❙
theory Fixpoints : ur:?LF =
include ?AllSets ❙
is_fixpoint: {A:type, f:A ⟶ A, a:A} prop ❘ = [A,f,a] f a ≐ a ❙
fixpoints: {A:type} (A ⟶ A) ⟶ set A ❘ = [A,f] ι [s] ∀[x] x ∈ s ⇒ is_fixpoint A f x ❙
theory POSet : base:?Logic =
include ?PrOSet ❙
......@@ -70,3 +81,4 @@ theory POSet : base:?Logic =
poset = Mod poset_theory ❘ role abbreviation ❙
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment