Package parser-all-def: Definition of the whole stream parser
Information
| name | parser-all-def |
| version | 1.90 |
| description | Definition of the whole stream parser |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2014-11-04 |
| checksum | 3658f9e60de4a861dbcba7a2f59bee1960633787 |
| requires | bool option pair parser-comb parser-stream |
| show | Data.Bool Data.Option Data.Pair Parser Parser.Stream |
Files
- Package tarball parser-all-def-1.90.tgz
- Theory source file parser-all-def.thy (included in the package tarball)
Defined Constant
- Parser
- parseStream
Theorems
⊦ ∀p. parseStream p eof = eof
⊦ ∀p. parseStream p error = error
⊦ ∀p a s.
parseStream p (cons a s) =
case destParser p a s of
none → error
| some (b, s') → cons b (parseStream p s')
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
- destParser
- Stream
- case
- cons
- eof
- error
- isProperSuffix
- isSuffix
Assumptions
⊦ ⊤
⊦ (∃) = λp. p ((select) p)
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀t. t ⇒ ⊤ ⇔ ⊤
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀b f. case b f none = b
⊦ ∀p x. p x ⇒ p ((select) p)
⊦ ∀x. ∃a b. x = (a, b)
⊦ ∀x. x = none ∨ ∃a. x = some a
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ ∀e b f. case e b f eof = b
⊦ ∀e b f. case e b f error = e
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀b f a. case b f (some a) = f a
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀s s'. isSuffix s s' ⇔ s = s' ∨ isProperSuffix s s'
⊦ ∀f. ∃fn. ∀a b. fn (a, b) = f a b
⊦ ∀r. (∀x. ∃y. r x y) ⇔ ∃f. ∀x. r x (f x)
⊦ ∀s a s'. isProperSuffix s (cons a s') ⇔ s = s' ∨ isProperSuffix s s'
⊦ ∀x. x = error ∨ x = eof ∨ ∃a0 a1. x = cons a0 a1
⊦ ∀e b f a s. case e b f (cons a s) = f a s
⊦ ∀p q. (∀x. p x ∧ q x) ⇔ (∀x. p x) ∧ ∀x. q x
⊦ ∀p a s b s'. destParser p a s = some (b, s') ⇒ isSuffix s' s
⊦ ∀a0 a1 a0' a1'. cons a0 a1 = cons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
⊦ ∀h.
(∀f g s. (∀s'. isProperSuffix s' s ⇒ f s' = g s') ⇒ h f s = h g s) ⇒
∃f. ∀s. f s = h f s