Package parser-all-def: Definition of the whole stream parser
Information
| name | parser-all-def |
| version | 1.94 |
| description | Definition of the whole stream parser |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2015-02-26 |
| checksum | 53938d8a10b4940217dc33a586a174887914db9b |
| requires | base parser-comb parser-stream |
| show | Data.Bool Data.Option Data.Pair Parser Parser.Stream |
Files
- Package tarball parser-all-def-1.94.tgz
- Theory source file parser-all-def.thy (included in the package tarball)
Defined Constant
- Parser
- parse
Theorems
⊦ ∀p. parse p eof = eof
⊦ ∀p. parse p error = error
⊦ ∀p x xs.
parse p (cons x xs) =
case dest p x xs of none → error | some (y, ys) → cons y (parse p ys)
External Type Operators
- →
- bool
- Data
- Option
- option
- Pair
- ×
- Option
- Parser
- parser
- Stream
- stream
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ⊤
- Option
- case
- none
- some
- Pair
- ,
- Bool
- Parser
- dest
- Stream
- case
- cons
- eof
- error
- isProperSuffix
- isSuffix
Assumptions
⊦ ⊤
⊦ (∃) = λp. p ((select) p)
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. t ⇒ ⊤ ⇔ ⊤
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀b f. case b f none = b
⊦ ∀p x. p x ⇒ p ((select) p)
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀b f a. case b f (some a) = f a
⊦ ∀xs y ys. isProperSuffix xs (cons y ys) ⇔ isSuffix xs ys
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀f. ∃fn. ∀a b. fn (a, b) = f a b
⊦ ∀r. (∀x. ∃y. r x y) ⇔ ∃f. ∀x. r x (f x)
⊦ ∀xs. xs = error ∨ xs = eof ∨ ∃x xt. xs = cons x xt
⊦ ∀p q. (∀x. p x ∧ q x) ⇔ (∀x. p x) ∧ ∀x. q x
⊦ ∀p x xs.
dest p x xs = none ∨ ∃y ys. dest p x xs = some (y, ys) ∧ isSuffix ys xs
⊦ ∀h.
(∀f g xs.
(∀ys. isProperSuffix ys xs ⇒ f ys = g ys) ⇒ h f xs = h g xs) ⇒
∃fn. ∀xs. fn xs = h fn xs
⊦ (∀e b f. case e b f error = e) ∧ (∀e b f. case e b f eof = b) ∧
∀e b f x xs. case e b f (cons x xs) = f x xs