Package list-quant: List quantifiers
Information
| name | list-quant |
| version | 1.28 |
| description | List quantifiers |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| requires | bool function set list-def list-set list-append list-map |
| show | Data.Bool Data.List Function Set |
Files
- Package tarball list-quant-1.28.tgz
- Theory file list-quant.thy (included in the package tarball)
Defined Constants
- Data
- List
- all
- exists
- List
Theorems
⊦ ∀p. all p []
⊦ ∀l. all (λx. T) l
⊦ ∀p. ¬exists p []
⊦ ∀P l. ¬all P l ⇔ exists (λx. ¬P x) l
⊦ ∀P l. ¬exists P l ⇔ all (λx. ¬P x) l
⊦ ∀P l. all P l ⇔ ∀x. x ∈ toSet l ⇒ P x
⊦ ∀P l. exists P l ⇔ ∃x. x ∈ toSet l ∧ P x
⊦ ∀P f l. all P (map f l) ⇔ all (P ∘ f) l
⊦ ∀P f l. exists P (map f l) ⇔ exists (P ∘ f) l
⊦ ∀p h t. all p (h :: t) ⇔ p h ∧ all p t
⊦ ∀p h t. exists p (h :: t) ⇔ p h ∨ exists p t
⊦ ∀P l. (∀x. all (P x) l) ⇔ all (λs. ∀x. P x s) l
⊦ ∀P l. (∃x. exists (P x) l) ⇔ exists (λs. ∃x. P x s) l
⊦ ∀P l1 l2. all P (l1 @ l2) ⇔ all P l1 ∧ all P l2
⊦ ∀P Q l. (∀x. P x ⇒ Q x) ⇒ all P l ⇒ all Q l
⊦ ∀f g l. all (λx. f x = g x) l ⇒ map f l = map g l
⊦ ∀P Q l. all P l ∧ all Q l ⇔ all (λx. P x ∧ Q x) l
⊦ ∀P Q l. all (λx. P x ⇒ Q x) l ∧ all P l ⇒ all Q l
Input Type Operators
- →
- bool
- Data
- List
- list
- List
- Set
- set
Input Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- F
- T
- List
- ::
- @
- []
- map
- toSet
- Bool
- Function
- id
- ∘
- Set
- ∅
- insert
- ∈
Assumptions
⊦ T
⊦ ¬F ⇔ T
⊦ ¬T ⇔ F
⊦ toSet [] = ∅
⊦ F ⇔ ∀p. p
⊦ ∀x. ¬(x ∈ ∅)
⊦ ∀x. id x = x
⊦ (¬) = λp. p ⇒ F
⊦ (∃) = λp. p ((select) p)
⊦ ∀a. ∃x. x = a
⊦ ∀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. F ∧ t ⇔ F
⊦ ∀t. T ∧ t ⇔ t
⊦ ∀t. t ∧ T ⇔ t
⊦ ∀t. F ⇒ t ⇔ T
⊦ ∀t. T ⇒ t ⇔ t
⊦ ∀t. t ⇒ T ⇔ T
⊦ ∀t. F ∨ t ⇔ t
⊦ ∀t. T ∨ t ⇔ T
⊦ ∀t. t ∨ F ⇔ t
⊦ ∀t. t ∨ T ⇔ T
⊦ ∀l. [] @ l = l
⊦ ∀f. map f [] = []
⊦ ∀t. (F ⇔ t) ⇔ ¬t
⊦ ∀t. (t ⇔ F) ⇔ ¬t
⊦ ∀t. t ⇒ F ⇔ ¬t
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ T) ∨ (t ⇔ F)
⊦ ∀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
⊦ (∧) = λp q. (λf. f p q) = λf. f T T
⊦ ∀p. ¬(∀x. p x) ⇔ ∃x. ¬p x
⊦ ∀p. ¬(∃x. p x) ⇔ ∀x. ¬p x
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀h t. toSet (h :: t) = insert h (toSet t)
⊦ ∀f g x. (f ∘ g) x = f (g x)
⊦ ∀t1 t2. ¬(t1 ∧ t2) ⇔ ¬t1 ∨ ¬t2
⊦ ∀t1 t2. ¬(t1 ∨ t2) ⇔ ¬t1 ∧ ¬t2
⊦ ∀f g. (∀x. f x = g x) ⇔ f = g
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀p q. p ∧ (∃x. q x) ⇔ ∃x. p ∧ q x
⊦ ∀p q. p ∨ (∃x. q x) ⇔ ∃x. p ∨ q x
⊦ ∀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
⊦ ∀t1 t2 t3. (t1 ∧ t2) ∧ t3 ⇔ t1 ∧ t2 ∧ t3
⊦ ∀t1 t2 t3. (t1 ∨ t2) ∨ t3 ⇔ t1 ∨ t2 ∨ t3
⊦ ∀l h t. (h :: t) @ l = h :: t @ l
⊦ ∀p. (∀x. ∃y. p x y) ⇔ ∃y. ∀x. p x (y x)
⊦ ∀f h t. map f (h :: t) = f h :: map f t
⊦ ∀x y s. x ∈ insert y s ⇔ x = y ∨ x ∈ s
⊦ ∀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
⊦ ∀P. P [] ∧ (∀a0 a1. P a1 ⇒ P (a0 :: a1)) ⇒ ∀x. P x
⊦ ∀NIL' CONS'.
∃fn. fn [] = NIL' ∧ ∀a0 a1. fn (a0 :: a1) = CONS' a0 a1 (fn a1)