Package parser-comb-thm: Properties of stream parser combinators

Information

nameparser-comb-thm
version1.100
descriptionProperties of stream parser combinators
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2015-04-21
checksum0cded31f5d5b3933cff5214709bae92808b4d666
requiresbase
parser-comb-def
parser-stream
showData.Bool
Data.List
Data.Option
Data.Pair
Parser
Parser.Stream

Files

Theorems

p. invariant (dest p)

f. invariant (token.prs f)

p. invariant (sequence.prs p)

inverse any (λx. x :: [])

strongInverse any (λx. x :: [])

xs. apply none xs = none

p1 p2. invariant (orelse.prs p1 p2)

p f. invariant (mapPartial.prs p f)

p. filter any p = some p

f. mapPartial any f = token f

f. dest (token f) = token.prs f

p. dest (sequence p) = sequence.prs p

x xs. dest none x xs = none

p1 p2. dest (orelse p1 p2) = orelse.prs p1 p2

p f. dest (mapPartial p f) = mapPartial.prs p f

apply any = case none none (λx xs. some (x, xs))

x xs. dest any x xs = some (x, xs)

p1 p2. dest p1 = dest p2 p1 = p2

p.
    apply (some p) =
    case none none (λx xs. if p x then some (x, xs) else none)

f.
    apply (token f) =
    case none none (λx xs. case f x of none none | some y some (y, xs))

p x xs. dest (some p) x xs = if p x then some (x, xs) else none

f e. (x. f (e x) = some x) inverse (token f) (λx. e x :: [])

p1 p2 xs.
    apply (orelse p1 p2) xs =
    case apply p1 xs of none apply p2 xs | some yys some yys

p x xs y ys. dest p x xs = some (y, ys) isSuffix ys xs

p xs.
    apply p xs = none
    y ys. apply p xs = some (y, ys) isProperSuffix ys xs

p f g e.
    inverse p e (x. f (g x) = x) inverse (map p f) (λx. e (g x))

p xs.
    apply (sequence p) xs =
    case apply p xs of none none | some (y, ys) apply y ys

p f g e.
    inverse p e (x. f (g x) = some x)
    inverse (mapPartial p f) (λx. e (g x))

p x xs.
    dest p x xs = none y ys. dest p x xs = some (y, ys) isSuffix ys xs

p x xs.
    invariant p
    p x xs = none y ys. p x xs = some (y, ys) isSuffix ys xs

(p. apply p error = none) (p. apply p eof = none)
  p x xs. apply p (cons x xs) = dest p x xs

p f xs.
    apply (map p f) xs =
    case apply p xs of none none | some (y, ys) some (f y, ys)

p1 p2 e1 e2.
    inverse p1 e1 inverse p2 e2
    inverse (pair p1 p2) (λ(x1, x2). e1 x1 @ e2 x2)

p1 p2 e1 e2.
    strongInverse p1 e1 strongInverse p2 e2
    strongInverse (pair p1 p2) (λ(x1, x2). e1 x1 @ e2 x2)

p f xs.
    apply (filter p f) xs =
    case apply p xs of
      none none
    | some (y, ys) if f y then some (y, ys) else none

p f x xs.
    dest (map p f) x xs =
    case dest p x xs of none none | some (y, ys) some (f y, ys)

p f xs.
    apply (mapPartial p f) xs =
    case apply p xs of
      none none
    | some (y, ys) case f y of none none | some z some (z, ys)

p f x xs.
    dest (filter p f) x xs =
    case dest p x xs of
      none none
    | some (y, ys) if f y then some (y, ys) else none

f e.
    (x. f (e x) = some x)
    (y1 y2 x. f y1 = some x f y2 = some x y1 = y2)
    strongInverse (token f) (λx. e x :: [])

p f g e.
    strongInverse p e (x. f (g x) = x)
    (y1 y2 x. f y1 = x f y2 = x y1 = y2)
    strongInverse (map p f) (λx. e (g x))

p1 p2 xs.
    apply (pair p1 p2) xs =
    case apply p1 xs of
      none none
    | some (y, ys)
        case apply p2 ys of none none | some (z, zs) some ((y, z), zs)

p f g e.
    strongInverse p e (x. f (g x) = some x)
    (y1 y2 x. f y1 = some x f y2 = some x y1 = y2)
    strongInverse (mapPartial p f) (λx. e (g x))

p1 p2 x xs.
    dest (pair p1 p2) x xs =
    case dest p1 x xs of
      none none
    | some (y, ys)
        case apply p2 ys of none none | some (z, zs) some ((y, z), zs)

External Type Operators

External Constants

Assumptions

t. t t

xs. isSuffix xs xs

p. p

any = some (Function.const )

none = token (Function.const none)

(¬) = λp. p

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

a. ¬(some a = none)

t. t t

t. t t

t. t

t. t t

t. t

t. t t

t. t

a. mk (dest a) = a

p. apply p eof = none

p. apply p error = none

f. token f = mk (token.prs f)

p. sequence p = mk (sequence.prs p)

x y. Function.const x y = x

() = λp q. p q p

t. (t ) (t )

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

b f. case b f none = b

p x. p x p ((select) p)

f y. (let x y in f x) = f y

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

p1 p2. orelse p1 p2 = mk (orelse.prs p1 p2)

p f. mapPartial p f = mk (mapPartial.prs p f)

() = λp q. (λf. f p q) = λf. f

() = λp. q. (x. p x q) q

a b. some a = some b a = b

p. some p = token (λx. if p x then some x else none)

b f a. case b f (some a) = f a

p f. map p f = mapPartial p (λx. some (f x))

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

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

() = λ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 ys zs. append (xs @ ys) zs = append xs (append ys zs)

xs ys zs. isSuffix xs ys isSuffix ys zs isSuffix xs zs

p f. filter p f = mapPartial p (λx. if f x then some x else none)

p1 p2. pair p1 p2 = sequence (map p1 (λx. map p2 (λy. (x, y))))

xs. xs = error xs = eof x xt. xs = cons x xt

f x xs.
    token.prs f x xs = case f x of none none | some y some (y, xs)

p q. (x. p x q x) (x. p x) x. q x

a b a' b'. (a, b) = (a', b') a = a' b = b'

x xs y ys. cons x xs = cons y ys x = y xs = ys

p e. inverse p e x xs. apply p (append (e x) xs) = some (x, xs)

p c x y. p (if c then x else y) (c p x) (¬c p y)

(xs. append [] xs = xs)
  h t xs. append (h :: t) xs = cons h (append t xs)

p1 p2 x xs.
    orelse.prs p1 p2 x xs =
    case dest p1 x xs of none dest p2 x xs | some yys some yys

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

p x xs.
    sequence.prs p x xs =
    case dest p x xs of none none | some (q, ys) apply q ys

p e.
    strongInverse p e
    inverse p e
    xs y ys. apply p xs = some (y, ys) xs = append (e y) ys

p f x xs.
    mapPartial.prs p f x xs =
    case dest p x xs of
      none none
    | some (y, ys) case f y of none none | some z some (z, ys)

(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