Package parser-fold-thm: Properties of the fold parsers

Information

nameparser-fold-thm
version1.3
descriptionProperties of the fold parsers
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2015-03-06
checksumcfb4489e563ba9182bc6dba93ec3e74907d9bdb3
requiresbase
parser-comb
parser-fold-def
parser-stream
showData.Bool
Data.Option
Data.Pair
Data.Sum
Parser
Parser.Stream

Files

Theorems

f s. invariant (fold.prs f s)

f. fold f = Function.∘ mk (fold.prs f)

f s. dest (fold f s) = fold.prs f s

f s. apply (fold f s) = case none none (λx xs. fold.prs f s x xs)

External Type Operators

External Constants

Assumptions

xs. isSuffix xs xs

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. t t

t. t

p. apply p eof = none

p. apply p error = none

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

r. invariant r dest (mk r) = r

x y. x = y y = x

xs ys. isProperSuffix xs ys isSuffix xs ys

x. x = none a. x = some a

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

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

f g x. Function.∘ f g x = f (g x)

xs y ys. isProperSuffix xs (cons y ys) isSuffix xs ys

f g. (x. f x = g x) f = g

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

p x xs. apply p (cons x xs) = dest p x xs

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. p error p eof (x xs. p xs p (cons x xs)) xs. p xs

p.
    invariant p
    x xs. case p x xs of none | some (y, ys) isSuffix ys xs

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

(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