Package relation: Relation operators

Information

namerelation
version1.39
descriptionRelation operators
authorJoe Hurd <joe@gilith.com>
licenseMIT
requiresbool
function
natural
pair
set
showData.Bool
Data.Pair
Function
Number.Natural
Relation

Files

Defined Constants

Theorems

irreflexive empty

irreflexive isSuc

reflexive universe

transitive empty

transitive universe

transitive (<)

wellFounded empty

wellFounded (<)

wellFounded isSuc

subrelation isSuc (<)

empty = fromSet Set.∅

universe = fromSet Set.universe

transitiveClosure isSuc = (<)

m. wellFounded (measure m)

r. transitive (transitiveClosure r)

r. subrelation r r

r. subrelation r (transitiveClosure r)

x y. universe x y

s. toSet (fromSet s) = s

r. wellFounded r irreflexive r

r. fromSet (toSet r) = r

x y. ¬empty x y

r x. reflexive r r x x

r. reflexive r x. r x x

s. bigIntersect s = fromSet (Set.bigIntersect (Set.image toSet s))

s. bigUnion s = fromSet (Set.bigUnion (Set.image toSet s))

r x. irreflexive r ¬r x x

r. irreflexive r x. ¬r x x

m n. isSuc m n suc m = n

r. subrelation isSuc r transitive r subrelation (<) r

r s. subrelation r s wellFounded s wellFounded r

r s. subrelation r s Set.⊆ (toSet r) (toSet s)

r s. toSet r = toSet s r = s

r s. intersect r s = fromSet (Set.∩ (toSet r) (toSet s))

r s. union r s = fromSet (Set.∪ (toSet r) (toSet s))

r m. wellFounded r wellFounded (λx y. r (m x) (m y))

r s.
    subrelation r s transitive s subrelation (transitiveClosure r) s

r s. subrelation r s subrelation s r r = s

m x y. measure m x y m x < m y

s x y. fromSet s x y Set.∈ (x, y) s

r. wellFounded r ¬f. n. r (f (suc n)) (f n)

r x y. Set.∈ (x, y) (toSet r) r x y

r s t. subrelation r s subrelation s t subrelation r t

r s. subrelation r (bigIntersect s) t. Set.∈ t s subrelation r t

r s. subrelation r s x y. r x y s x y

r s. (x y. r x y s x y) r = s

r. toSet r = { x y. x, y | r x y }

s x y. bigIntersect s x y r. Set.∈ r s r x y

s x y. bigUnion s x y r. Set.∈ r s r x y

p g h. f. x. f x = if p x then f (g x) else h x

r.
    transitiveClosure r =
    bigIntersect { s. s | subrelation r s transitive s }

r s x y. intersect r s x y r x y s x y

r s x y. union r s x y r x y s x y

r. transitive r x y z. r x y r y z r x z

m a b. (y. measure m y a measure m y b) m a m b

r. wellFounded r p. (x. (y. r y x p y) p x) x. p x

r. wellFounded r p. (x. p x) x. p x y. r y x ¬p y

r. wellFounded r p. (x. p x) x. p x y. r y x ¬p y

r s.
    wellFounded r wellFounded s
    wellFounded (λ(x1, y1) (x2, y2). r x1 x2 s y1 y2)

r.
    wellFounded r
    h.
      (f g x. (z. r z x f z = g z) h f x = h g x)
      ∃!f. x. f x = h f x

r s.
    wellFounded r wellFounded s
    wellFounded (λ(x1, y1) (x2, y2). r x1 x2 x1 = x2 s y1 y2)

r.
    (x. ¬r x x) (x y z. r x y r y z r x z)
    (x. Set.finite { y. y | r y x }) wellFounded r

r s.
    wellFounded r (a. wellFounded (s a))
    wellFounded (λ(x1, y1) (x2, y2). r x1 x2 x1 = x2 s x1 y1 y2)

Input Type Operators

Input Constants

Assumptions

Set.infinite Set.universe

¬

¬

x. Set.∈ x Set.universe

t. t t

p. p

x. ¬Set.∈ x Set.∅

x. id x = x

t. t ¬t

n. ¬(n < n)

n. 0 < suc n

n. n < suc n

(¬) = λp. p

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

m. m < 0

m. m + 0 = m

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

s. Set.infinite s ¬Set.finite s

() = λp q. p q p

t. (t ) (t )

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

p x. p x p ((select) p)

f y. (let x y in f x) = f y

x y. x = y y = x

t1 t2. t1 t2 t2 t1

t1 t2. t1 t2 t2 t1

s x. Set.finite (Set.insert x s) Set.finite s

p x. Set.∈ x (Set.fromPredicate p) p x

m n. ¬(m n) n < m

m. m = 0 n. m = suc n

() = λp q. (λf. f p q) = λf. f

p. ¬(x. p x) x. ¬p x

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

t1 t2. ¬(t1 t2) t1 ¬t2

t1 t2. ¬t1 ¬t2 t2 t1

m n. m + suc n = suc (m + n)

m n. suc m < suc n m < n

s t. Set.finite t Set.⊆ s t Set.finite s

t1 t2. ¬(t1 t2) ¬t1 ¬t2

p. (xy. p xy) x y. p (x, y)

f g. (x. f x = g x) f = g

() = λp q. r. (p r) (q r) r

m n. m < n n < m m = n

s t. Set.⊆ s t Set.⊆ t s s = t

f. fn. x y. fn (x, y) = f x y

m n. m < n d. n = m + suc d

p q. (x. p q x) p x. q x

p q. (x. p q x) p x. q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

m n. m < suc n m = n m < n

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

p q r. p q r p q r

t1 t2 t3. (t1 t2) t3 t1 t2 t3

t1 t2 t3. (t1 t2) t3 t1 t2 t3

m n p. m < n n < p m < p

m n p. m < n n p m < p

s t u. Set.⊆ s t Set.⊆ t u Set.⊆ s u

s t. Set.⊆ s t x. Set.∈ x s Set.∈ x t

s t. (x. Set.∈ x s Set.∈ x t) s = t

p x. (y. p y y = x) (select) p = x

p. (x. y. p x y) y. x. p x (y x)

t f. Set.⊆ t (Set.bigIntersect f) s. Set.∈ s f Set.⊆ t s

p. p 0 (n. p n p (suc n)) n. p n

s x. Set.∈ x (Set.bigIntersect s) t. Set.∈ t s Set.∈ x t

s x. Set.∈ x (Set.bigUnion s) t. Set.∈ t s Set.∈ x t

p x. Set.∈ x { y. y | p y } p x

x y s. Set.∈ x (Set.insert y s) x = y Set.∈ x s

s t x. Set.∈ x (Set.∩ s t) Set.∈ x s Set.∈ x t

s t x. Set.∈ x (Set.∪ s t) Set.∈ x s Set.∈ x t

(∃!) = λp. () p x y. p x p y x = y

P. (n. (m. m < n P m) P n) n. P n

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x) (x. q x) x. p x q x

e f. ∃!fn. fn 0 = e n. fn (suc n) = f (fn n) n

y s f. Set.∈ y (Set.image f s) x. y = f x Set.∈ x s

x y a b. (x, y) = (a, b) x = a y = b

p1 p2 q1 q2. (p1 p2) (q1 q2) p1 q1 p2 q2

p1 p2 q1 q2. (p2 p1) (q1 q2) (p1 q1) p2 q2

p c x y. p (if c then x else y) (c p x) (¬c p y)

f s.
    (x y. f x = f y x = y) Set.infinite s
    Set.infinite (Set.image f s)

p f s. (y. Set.∈ y (Set.image f s) p y) x. Set.∈ x s p (f x)