Package parser-fold-def: Definition of the fold parsers

Information

name	parser-fold-def
version	1.2
description	Definition of the fold parsers
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2015-03-05
checksum	610ab92af560e127e0d47ae37fba37aaa1681aac
requires	base parser-comb parser-stream
show	Data.Bool Data.Option Data.Pair Data.Sum Number.Natural Parser Parser.Stream

Files

Package tarball parser-fold-def-1.2.tgz
Theory source file parser-fold-def.thy (included in the package tarball)

Defined Constants

Parser
- fold
  - fold.prs
- foldN

Theorems

⊦ ∀f s. fold f s = mk (fold.prs f s)

⊦ ∀f s x xs.
    fold.prs f s x xs =
    case f x s of
      none → none
    | some y →
        case y of
          left z → some (z, xs)
        | right t →
            case xs of
              error → none
            | eof → none
            | cons z zs → fold.prs f t z zs

⊦ ∀f n s.
    foldN f n s =
    fold
      (λx (m, t).
         map (λu. if m = 0 then left u else right (m - 1, u)) (f x t))
      (n, s)

External Type Operators

→
bool
Data
- Option
  - option
- Pair
  - ×
- Sum
  - +
Number
- Natural
  - natural
Parser
- parser
- Stream
  - stream

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - cond
  - ⊥
  - ⊤
- Option
  - case
  - map
  - none
  - some
- Pair
  - ,
- Sum
  - case
  - left
  - right
Number
- Natural
  - -
  - bit1
  - zero
Parser
- mk
- Stream
  - case
  - cons
  - eof
  - error

Assumptions

⊦ ⊤

⊦ (∃) = λp. p ((select) p)

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

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

⊦ ∀t. t ⇒ ⊤ ⇔ ⊤

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

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

⊦ ∀b f. case b f none = b

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

⊦ ∀x. x = none ∨ ∃a. x = some a

⊦ (∧) = λ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

⊦ ∀f g a. case f g (left a) = f a

⊦ ∀f g b. case f g (right b) = g b

⊦ ∀x. (∃a. x = left a) ∨ ∃b. x = right b

⊦ (∨) = λ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 g h. ∃f. ∀x. f x = if p x then f (g x) else h x

⊦ (∀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