Package parser-all-thm: Properties of the whole stream parser

Information

nameparser-all-thm
version1.105
descriptionProperties of the whole stream parser
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2015-04-21
checksum88706fe6f8dd950c770a86961fe576b561b771f3
requiresbase
parser-all-def
parser-comb
parser-stream
showData.Bool
Data.List
Data.Option
Data.Pair
Number.Natural
Parser
Parser.Stream

Files

Theorems

p xs. length (parse p xs) length xs

p f xs. parse (map p f) xs = map f (parse p xs)

p e l. inverse p e parse p (fromList (concat (map e l))) = fromList l

p e x xs. inverse p e parse p (append (e x) xs) = cons x (parse p xs)

p e xs ys ye.
    strongInverse p e toList (parse p xs) = (ys, ye)
    ye xs = fromList (concat (map e ys))

p xs.
    parse p xs =
    case apply p xs of
      none case xs of error error | eof eof | cons y ys error
    | some (y, ys) cons y (parse p ys)

(p. parse p error = error) (p. parse p eof = eof)
  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

External Constants

Assumptions

¬

length eof = 0

length error = 0

concat [] = []

n. 0 n

n. n n

p. p

t. t ¬t

xs. ¬isProperSuffix xs xs

(¬) = λp. p

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

f. map f [] = []

p. parse p eof = eof

p. parse p error = error

p. apply p eof = none

p. apply p error = none

t. t ¬t

l. fromList l = append l eof

() = λ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 xs. length (cons x xs) = suc (length xs)

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

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

a b. some a = some b a = b

m n. suc m suc n m n

h t. concat (h :: t) = h @ concat t

xs ys. isSuffix xs ys length xs length ys

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

l. l = [] h t. l = h :: t

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

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

m n p. m n n p m p

xs ys zs. append (xs @ ys) zs = append xs (append ys zs)

f h t. map f (h :: t) = f h :: map f t

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

p. (xs. (ys. isProperSuffix ys xs p ys) p xs) xs. p xs

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

p. p [] (h t. p t p (h :: t)) l. p l

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

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

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

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

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

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

p x xs.
    parse p (cons x xs) =
    case dest p x xs of none error | some (y, ys) cons y (parse p ys)

(f. map f error = error) (f. map f eof = eof)
  f x xs. map f (cons x xs) = cons (f x) (map f xs)

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)

toList error = ([], ) toList eof = ([], )
  x xs. toList (cons x xs) = let (l, e) toList xs in (x :: l, e)

(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