Package axiom: Standard axioms

Information

name	axiom
version	1.11
description	Standard axioms
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
requires	bool function
show	Data.Bool Function

Files

Package tarball axiom-1.11.tgz
Theory file axiom.thy (included in the package tarball)

Theorems

⊦ ∀t. (λx. t x) = t

⊦ ∃f. injective f ∧ ¬surjective f

⊦ ∀p x. p x ⇒ p ((select) p)

Input Type Operators

→
bool
ind

Input Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ¬
  - ⊥
  - ⊤
Function
- injective
- surjective

Assumptions

⊦ ⊤

⊦ ⊥ ⇔ ∀p. p

⊦ (¬) = λp. p ⇒ ⊥

⊦ ⊤ ⇔ (λp. p) = λp. p

⊦ (∀) = λp. p = λx. ⊤

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ ∀f. surjective f ⇔ ∀y. ∃x. y = f x

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ let a d ← (λe. d e) = d in a = λb. (λc. c) = λc. c

⊦ ∀f. injective f ⇔ ∀x₁ x₂. f x₁ = f x₂ ⇒ x₁ = x₂

⊦ let a d ←
      let e g ←
          (let h ← d g in
           λi.
             (let j ← h in
              λk. (λl. l j k) = λm. m ((λc. c) = λc. c) ((λc. c) = λc. c))
               i ⇔ h) (d ((select) d)) in
      e = (λf. (λc. c) = λc. c) in
  a = λb. (λc. c) = λc. c

⊦ let a o ←
      (let h ←
           let p r ←
               let p s ←
                   (let f ← o r = o s in
                    λg.
                      (let h ← f in
                       λi.
                         (λj. j h i) =
                         λk. k ((λd. d) = λd. d) ((λd. d) = λd. d)) g ⇔ f)
                     (r = s) in
               p = (λq. (λd. d) = λd. d) in
           p = (λq. (λd. d) = λd. d) in
       λi. (λj. j h i) = λk. k ((λd. d) = λd. d) ((λd. d) = λd. d))
        (let t ←
             let p u ←
                 let v y ← u = o y in
                 let b w ←
                     (let f ←
                          let p x ←
                              (let f ← v x in
                               λg.
                                 (let h ← f in
                                  λi.
                                    (λj. j h i) =
                                    λk.
                                      k ((λd. d) = λd. d)
                                        ((λd. d) = λd. d)) g ⇔ f) w in
                          p = (λq. (λd. d) = λd. d) in
                      λg.
                        (let h ← f in
                         λi.
                           (λj. j h i) =
                           λk. k ((λd. d) = λd. d) ((λd. d) = λd. d)) g ⇔
                        f) w in
                 b = (λc. (λd. d) = λd. d) in
             p = (λq. (λd. d) = λd. d) in
         (let f ← t in
          λg.
            (let h ← f in
             λi. (λj. j h i) = λk. k ((λd. d) = λd. d) ((λd. d) = λd. d))
              g ⇔ f) (let b d ← d in b = λc. (λd. d) = λd. d)) in
  let b e ←
      (let f ←
           let l n ←
               (let f ← a n in
                λg.
                  (let h ← f in
                   λi.
                     (λj. j h i) =
                     λk. k ((λd. d) = λd. d) ((λd. d) = λd. d)) g ⇔ f) e in
           l = (λm. (λd. d) = λd. d) in
       λg.
         (let h ← f in
          λi. (λj. j h i) = λk. k ((λd. d) = λd. d) ((λd. d) = λd. d)) g ⇔
         f) e in
  b = λc. (λd. d) = λd. d