Package char-utf8: The UTF-8 encoding of Unicode characters

Information

Files

• Package tarball char-utf8-1.98.tgz
• Theory source file char-utf8.thy (included in the package tarball)

Defined Constants

• Data
  • Char
    • UTF8
      • decode
      • decodeStream
      • decoder
        • decoder.decode1
        • decoder.decode2
        • decoder.decode3
        • decoder.parse
      • encode
      • encoder
        • encoder.encode1
        • encoder.encode2
        • encoder.encode3
      • isContinuationByte
      • parseContinuationByte
      • parseThreeContinuationBytes
      • parseTwoContinuationBytes

Theorems

⊦ isParser decoder.parse

⊦ inverse decoder encoder

⊦ strongInverse decoder encoder

⊦ parseContinuationByte = parseSome isContinuationByte

⊦ decoder = mkParser decoder.parse

⊦ decodeStream = parseStream decoder

⊦ destParser decoder = decoder.parse

⊦ parseTwoContinuationBytes =
  parsePair parseContinuationByte parseContinuationByte

⊦ parseThreeContinuationBytes =
  parsePair parseContinuationByte parseTwoContinuationBytes

⊦ parse decoder = case none none decoder.parse

⊦ ∀cs. length cs ≤ length (encode cs)

⊦ ∀cs. decode (encode cs) = some cs

⊦ ∀bs. length (decodeStream bs) ≤ length bs

⊦ ∀bs. decode bs = toList (decodeStream (fromList bs))

⊦ ∀chs. encode chs = concat (map encoder chs)

⊦ ∀bs. case decode bs of none → ⊤ | some cs → encode cs = bs

⊦ ∀bs. case decode bs of none → ⊤ | some cs → length cs ≤ length bs

⊦ ∀b. isContinuationByte b ⇔ bit b 7 ∧ ¬bit b 6

⊦ ∀p₁ p₀.
    encoder.encode1 p₁ p₀ =
    let b₀₀ ← shiftLeft p₁ 2 in
    let b₀₁ ← shiftRight (and p₀ 192) 6 in
    let b₀ ← or 192 (or b₀₀ b₀₁) in
    let b₁₀ ← and p₀ 63 in
    let b₁ ← or 128 b₁₀ in
    b₀ :: b₁ :: []

⊦ ∀b₀ b₁.
    decoder.decode1 b₀ b₁ =
    let pl ← mkPlane 0 in
    let p₁ ← shiftRight (and b₀ 28) 2 in
    let y₀ ← shiftLeft (and b₀ 3) 6 in
    let x₀ ← and b₁ 63 in
    let p₀ ← or y₀ x₀ in
    if p₁ = 0 ∧ ¬bit p₀ 7 then none
    else
      let pos ← mkPosition (fromBytes p₀ p₁) in
      let ch ← mkChar (pl, pos) in
      some ch

⊦ ∀ch.
    encoder ch =
    let (pl, pos) ← destChar ch in
    let p ← destPlane pl in
    let (p₀, p₁) ← toBytes (destPosition pos) in
    if p = 0 then
      if p₁ = 0 ∧ ¬bit p₀ 7 then p₀ :: []
      else if and 248 p₁ = 0 then encoder.encode1 p₁ p₀
      else encoder.encode2 p₁ p₀
    else encoder.encode3 p p₁ p₀

⊦ ∀b₀ s.
    decoder.parse b₀ s =
    if bit b₀ 7 then
      if bit b₀ 6 then
        if bit b₀ 5 then
          if bit b₀ 4 then
            if bit b₀ 3 then none
            else
              parse
                (partialMap (decoder.decode3 b₀)
                   parseThreeContinuationBytes) s
          else
            parse
              (partialMap (decoder.decode2 b₀) parseTwoContinuationBytes) s
        else
          parse (partialMap (decoder.decode1 b₀) parseContinuationByte) s
      else none
    else
      let pl ← mkPlane 0 in
      let pos ← mkPosition (fromBytes b₀ 0) in
      let ch ← mkChar (pl, pos) in
      some (ch, s)

⊦ ∀p₁ p₀.
    encoder.encode2 p₁ p₀ =
    let b₀₀ ← shiftRight (and p₁ 240) 4 in
    let b₀ ← or 224 b₀₀ in
    let b₁₀ ← shiftLeft (and p₁ 15) 2 in
    let b₁₁ ← shiftRight (and p₀ 192) 6 in
    let b₁ ← or 128 (or b₁₀ b₁₁) in
    let b₂₀ ← and p₀ 63 in
    let b₂ ← or 128 b₂₀ in
    b₀ :: b₁ :: b₂ :: []

⊦ ∀b₀ b₁ b₂ b₃.
    decoder.decode3 b₀ (b₁, b₂, b₃) =
    let w ← shiftLeft (and b₀ 7) 2 in
    let z ← shiftRight (and b₁ 48) 4 in
    let p ← or w z in
    if p = 0 ∨ 16 < p then none
    else
      let pl ← mkPlane p in
      let z₁ ← shiftLeft (and b₁ 15) 4 in
      let y₁ ← shiftRight (and b₂ 60) 2 in
      let p₁ ← or z₁ y₁ in
      let y₀ ← shiftLeft (and b₂ 3) 6 in
      let x₀ ← and b₃ 63 in
      let p₀ ← or y₀ x₀ in
      let pos ← mkPosition (fromBytes p₀ p₁) in
      let ch ← mkChar (pl, pos) in
      some ch

⊦ ∀b₀ b₁ b₂.
    decoder.decode2 b₀ (b₁, b₂) =
    let z₁ ← shiftLeft (and b₀ 15) 4 in
    let y₁ ← shiftRight (and b₁ 60) 2 in
    let p₁ ← or z₁ y₁ in
    if p₁ < 8 ∨ 216 ≤ p₁ ∧ p₁ ≤ 223 then none
    else
      let y₀ ← shiftLeft (and b₁ 3) 6 in
      let x₀ ← and b₂ 63 in
      let p₀ ← or y₀ x₀ in
      if p₁ = 255 ∧ 254 ≤ p₀ then none
      else
        let pl ← mkPlane 0 in
        let pos ← mkPosition (fromBytes p₀ p₁) in
        let ch ← mkChar (pl, pos) in
        some ch

⊦ ∀p p₁ p₀.
    encoder.encode3 p p₁ p₀ =
    let b₀₀ ← shiftRight (and p 28) 2 in
    let b₀ ← or 240 b₀₀ in
    let b₁₀ ← shiftLeft (and p 3) 4 in
    let b₁₁ ← shiftRight (and p₁ 240) 4 in
    let b₁ ← or 128 (or b₁₀ b₁₁) in
    let b₂₀ ← shiftLeft (and p₁ 15) 2 in
    let b₂₁ ← shiftRight (and p₀ 192) 6 in
    let b₂ ← or 128 (or b₂₀ b₂₁) in
    let b₃₀ ← and p₀ 63 in
    let b₃ ← or 128 b₃₀ in
    b₀ :: b₁ :: b₂ :: b₃ :: []

External Type Operators

• →
• bool
• Data
  • Byte
    • byte
  • Char
    • char
    • plane
    • position
  • List
    • list
  • Option
    • option
  • Pair
    • ×
  • Word16
    • word16
• Number
  • Natural
    • natural
• Parser
  • parser
  • Stream
    • stream

External Constants

• =
• select
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • cond
    • ⊥
    • ⊤
  • Byte
    • <
    • ≤
    • and
    • bit
    • fromNatural
    • or
    • shiftLeft
    • shiftRight
    • width
    • Bits
      • compare
      • fromByte
      • toByte
  • Char
    • destChar
    • destPlane
    • destPosition
    • isChar
    • isPlane
    • mkChar
    • mkPlane
    • mkPosition
  • List
    • ::
    • @
    • []
    • concat
    • drop
    • length
    • map
    • nth
    • replicate
    • take
    • zipWith
  • Option
    • case
    • none
    • some
  • Pair
    • ,
    • fst
    • snd
  • Word16
    • <
    • fromBytes
    • fromNatural
    • toBytes
    • width
    • Bits
      • compare
      • fromWord
      • toWord
• Number
  • Natural
    • *
    • +
    • -
    • <
    • ≤
    • ↑
    • bit0
    • bit1
    • div
    • even
    • mod
    • odd
    • suc
    • zero
• Parser
  • destParser
  • inverse
  • isParser
  • mkParser
  • parse
  • parsePair
  • parseSome
  • parseStream
  • partialMap
  • strongInverse
  • Stream
    • append
    • case
    • cons
    • eof
    • error
    • fromList
    • isProperSuffix
    • isSuffix
    • length
    • toList

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ length [] = 0

⊦ bit0 0 = 0

⊦ ∀x. x = x

⊦ ∀t. t ⇒ t

⊦ ∀n. 0 ≤ n

⊦ ∀n. n ≤ n

⊦ ∀x. isSuffix x x

⊦ ⊥ ⇔ ∀p. p

⊦ toByte [] = 0

⊦ toWord [] = 0

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ ⊥

⊦ ∀t. (∀x. t) ⇔ t

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

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

⊦ ∀a. ¬(some a = none)

⊦ ∀x. replicate x 0 = []

⊦ ∀t. ¬¬t ⇔ t

⊦ ∀t. (⊤ ⇔ t) ⇔ t

⊦ ∀t. (t ⇔ ⊤) ⇔ t

⊦ ∀t. ⊥ ∧ t ⇔ ⊥

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. t ∧ ⊥ ⇔ ⊥

⊦ ∀t. t ∧ ⊤ ⇔ t

⊦ ∀t. t ∧ t ⇔ t

⊦ ∀t. ⊥ ⇒ t ⇔ ⊤

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀t. t ⇒ ⊤ ⇔ ⊤

⊦ ∀t. ⊥ ∨ t ⇔ t

⊦ ∀t. ⊤ ∨ t ⇔ ⊤

⊦ ∀t. t ∨ ⊥ ⇔ t

⊦ ∀t. t ∨ ⊤ ⇔ ⊤

⊦ ∀r. destPosition (mkPosition r) = r

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. 0 * n = 0

⊦ ∀m. m * 0 = 0

⊦ ∀n. 0 + n = n

⊦ ∀m. m + 0 = m

⊦ ∀l. [] @ l = l

⊦ ∀l. drop 0 l = l

⊦ ∀l. take 0 l = []

⊦ ∀s. append [] s = s

⊦ ∀p. parse p eof = none

⊦ ∀p. parse p error = none

⊦ width = 8

⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t

⊦ ∀t. (t ⇔ ⊥) ⇔ ¬t

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

⊦ ∀q. compare q [] [] ⇔ q

⊦ ∀q. compare q [] [] ⇔ q

⊦ ∀n. bit1 n = suc (bit0 n)

⊦ ∀m. m ↑ 0 = 1

⊦ ∀m. m * 1 = m

⊦ ∀m. 1 * m = m

⊦ ∀l. length (fromList l) = length l

⊦ ∀l. toList (fromList l) = some l

⊦ ∀f. zipWith f [] [] = []

⊦ ∀m n. m ≤ m + n

⊦ width = 16

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

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

⊦ ∀n. even (suc n) ⇔ ¬even n

⊦ ∀n. odd (suc n) ⇔ ¬odd n

⊦ ∀m. m ≤ 0 ⇔ m = 0

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

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

⊦ ∀a b. fst (a, b) = a

⊦ ∀a b. snd (a, b) = b

⊦ ∀b f. case b f none = b

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

⊦ ∀r. isPlane r ⇔ destPlane (mkPlane r) = r

⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))

⊦ ∀r. isChar r ⇔ destChar (mkChar r) = r

⊦ ∀r. isParser r ⇔ destParser (mkParser r) = r

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀x y. x = y ⇒ y = x

⊦ ∀h t. nth (h :: t) 0 = h

⊦ ∀t₁ t₂. t₁ ∨ t₂ ⇔ t₂ ∨ t₁

⊦ ∀m n. m * n = n * m

⊦ ∀m n. m + n = n + m

⊦ ∀m n. m + n - n = m

⊦ ∀x y. isProperSuffix x y ⇒ isSuffix x y

⊦ ∀p s. length (parseStream p s) ≤ length s

⊦ ∀n. n ↑ 2 = n * n

⊦ ∀n. 2 * n = n + n

⊦ ∀h t. length (h :: t) = suc (length t)

⊦ ∀m n. ¬(m < n ∧ n ≤ m)

⊦ ∀m n. ¬(m ≤ n ∧ n < m)

⊦ ∀m n. ¬(m ≤ n) ⇔ n < m

⊦ ∀m n. suc m ≤ n ⇔ m < n

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

⊦ ∀s. case toList s of none → ⊤ | some l → length l = length s

⊦ (∧) = λ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. ¬(∀x. p x) ⇔ ∃x. ¬p x

⊦ ∀p. ¬(∃x. p x) ⇔ ∀x. ¬p x

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ ∀a a'. some a = some a' ⇔ a = a'

⊦ ∀w₁ w₂. fromByte w₁ = fromByte w₂ ⇔ w₁ = w₂

⊦ ∀pos. ∃w. pos = mkPosition w ∧ destPosition pos = w

⊦ ∀m n. m + suc n = suc (m + n)

⊦ ∀m n. suc m + n = suc (m + n)

⊦ ∀m n. suc m = suc n ⇔ m = n

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

⊦ ∀x n. replicate x (suc n) = x :: replicate x n

⊦ ∀t₁ t₂. ¬(t₁ ∧ t₂) ⇔ ¬t₁ ∨ ¬t₂

⊦ ∀t₁ t₂. ¬(t₁ ∨ t₂) ⇔ ¬t₁ ∧ ¬t₂

⊦ ∀w₁ w₂. compare ⊥ (fromByte w₁) (fromByte w₂) ⇔ w₁ < w₂

⊦ ∀w₁ w₂. compare ⊤ (fromByte w₁) (fromByte w₂) ⇔ w₁ ≤ w₂

⊦ ∀b₀ b₁. toWord (fromByte b₀ @ fromByte b₁) = fromBytes b₀ b₁

⊦ ∀w₁ w₂. compare ⊥ (fromWord w₁) (fromWord w₂) ⇔ w₁ < w₂

⊦ ∀m n. even (m * n) ⇔ even m ∨ even n

⊦ ∀m n. even (m + n) ⇔ even m ⇔ even n

⊦ ∀m n. m * suc n = m + m * n

⊦ ∀m n. m ↑ suc n = m * m ↑ n

⊦ ∀m n. suc m * n = m * n + n

⊦ ∀p. isPlane p ⇔ p < 17

⊦ ∀f g. (∀x. f x = g x) ⇔ f = g

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀w₁ w₂. and w₁ w₂ = toByte (zipWith (∧) (fromByte w₁) (fromByte w₂))

⊦ ∀w₁ w₂. or w₁ w₂ = toByte (zipWith (∨) (fromByte w₁) (fromByte w₂))

⊦ ∀m n. m ≤ n ⇔ m < n ∨ m = n

⊦ ∀m n. odd (m + n) ⇔ ¬(odd m ⇔ odd n)

⊦ ∀m n. m ≤ n ∧ n ≤ m ⇔ m = n

⊦ ∀l n. shiftLeft (toByte l) n = toByte (replicate ⊥ n @ l)

⊦ ∀f. ∃fn. ∀a b. fn (a, b) = f a b

⊦ ∀m n. m < n ⇔ ∃d. n = m + suc d

⊦ ∀p a s. parse p (cons a s) = destParser p a s

⊦ ∀p q. p ∨ (∃x. q x) ⇔ ∃x. p ∨ q x

⊦ ∀pl. ∃b. isPlane b ∧ pl = mkPlane b ∧ destPlane pl = b

⊦ ∀h t s. append (h :: t) s = cons h (append t s)

⊦ ∀t₁ t₂ t₃. (t₁ ∨ t₂) ∨ t₃ ⇔ t₁ ∨ t₂ ∨ t₃

⊦ ∀m n p. m * (n * p) = n * (m * p)

⊦ ∀m n p. m * (n * p) = m * n * p

⊦ ∀m n p. m + (n + p) = m + n + p

⊦ ∀n. toByte (odd n :: fromByte (fromNatural (n div 2))) = fromNatural n

⊦ ∀n. toWord (odd n :: fromWord (fromNatural (n div 2))) = fromNatural n

⊦ ∀l h t. (h :: t) @ l = h :: t @ l

⊦ ∀m n. m ≤ suc n ⇔ m = suc n ∨ m ≤ n

⊦ ∀m n. m * n = 0 ⇔ m = 0 ∨ n = 0

⊦ ∀w. ∃b₀ b₁. w = fromBytes b₀ b₁ ∧ toBytes w = (b₀, b₁)

⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n

⊦ ∀b t₁ t₂. (if b then t₁ else t₂) ⇔ (¬b ∨ t₁) ∧ (b ∨ t₂)

⊦ ∀m n p. m * (n + p) = m * n + m * p

⊦ ∀m n p. m ↑ (n + p) = m ↑ n * m ↑ p

⊦ ∀m n p. (m + n) * p = m * p + n * p

⊦ ∀x. x = error ∨ x = eof ∨ ∃a₀ a₁. x = cons a₀ a₁

⊦ ∀p.
    parse (parseSome p) =
    case none none (λa s. if p a then some (a, s) else none)

⊦ ∀b f x y. f (if b then x else y) = if b then f x else f y

⊦ ∀b f g x. (if b then f else g) x = if b then f x else g x

⊦ ∀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 q. (∃x. p x) ∨ (∃x. q x) ⇔ ∃x. p x ∨ q x

⊦ ∀p e l.
    inverse p e ⇒ parseStream p (fromList (concat (map e l))) = fromList l

⊦ ∀h t n. n < length t ⇒ nth (h :: t) (suc n) = nth t n

⊦ ∀n h t. n ≤ length t ⇒ drop (suc n) (h :: t) = drop n t

⊦ ∀m n p. m * n = m * p ⇔ m = 0 ∨ n = p

⊦ ∀m n p. m * n ≤ m * p ⇔ m = 0 ∨ n ≤ p

⊦ ∀l n. bit (toByte l) n ⇔ n < width ∧ n < length l ∧ nth l n

⊦ ∀m n p. m * n < m * p ⇔ ¬(m = 0) ∧ n < p

⊦ ∀h₁ h₂ t₁ t₂. h₁ :: t₁ = h₂ :: t₂ ⇔ h₁ = h₂ ∧ t₁ = t₂

⊦ ∀a b a' b'. (a, b) = (a', b') ⇔ a = a' ∧ b = b'

⊦ ∀p e. inverse p e ⇔ ∀x s. parse p (append (e x) s) = some (x, s)

⊦ ∀n h t. n ≤ length t ⇒ take (suc n) (h :: t) = h :: take n t

⊦ ∀l.
    fromByte (toByte l) =
    if length l ≤ width then l @ replicate ⊥ (width - length l)
    else take width l

⊦ ∀l.
    fromWord (toWord l) =
    if length l ≤ width then l @ replicate ⊥ (width - length l)
    else take width l

⊦ ∀c.
    ∃pl pos.
      isChar (pl, pos) ∧ c = mkChar (pl, pos) ∧ destChar c = (pl, pos)

⊦ ∀m n q r. m = q * n + r ∧ r < n ⇒ m div n = q

⊦ ∀m n q r. m = q * n + r ∧ r < n ⇒ m mod n = r

⊦ ∀p e s.
    strongInverse p e ⇒
    case toList (parseStream p s) of
      none → ⊤
    | some l → toList s = some (concat (map e l))

⊦ ∀w.
    (toByte (take 8 (fromWord w)), toByte (drop 8 (fromWord w))) =
    toBytes w

⊦ ∀p s.
    parse p s = none ∨
    ∃b s'. parse p s = some (b, s') ∧ isProperSuffix s' s

⊦ ∀p.
    isParser p ⇔
    ∀x xs. case p x xs of none → ⊤ | some (y, xs') → isSuffix xs' xs

⊦ ∀p e.
    strongInverse p e ⇔
    inverse p e ∧ ∀s x s'. parse p s = some (x, s') ⇒ s = append (e x) s'

⊦ ∀f h₁ h₂ t₁ t₂.
    length t₁ = length t₂ ⇒
    zipWith f (h₁ :: t₁) (h₂ :: t₂) = f h₁ h₂ :: zipWith f t₁ t₂

⊦ ∀q h₁ h₂ t₁ t₂.
    compare q (h₁ :: t₁) (h₂ :: t₂) ⇔
    compare (¬h₁ ∧ h₂ ∨ ¬(h₁ ∧ ¬h₂) ∧ q) t₁ t₂

⊦ ∀q h₁ h₂ t₁ t₂.
    compare q (h₁ :: t₁) (h₂ :: t₂) ⇔
    compare (¬h₁ ∧ h₂ ∨ ¬(h₁ ∧ ¬h₂) ∧ q) t₁ t₂

⊦ ∀b.
    ∃x₀ x₁ x₂ x₃ x₄ x₅ x₆ x₇.
      b = toByte (x₀ :: x₁ :: x₂ :: x₃ :: x₄ :: x₅ :: x₆ :: x₇ :: [])

⊦ ∀f p s.
    parse (partialMap f p) s =
    case parse p s of
      none → none
    | some (b, s') → case f b of none → none | some c → some (c, s')

⊦ ∀l n.
    shiftRight (toByte l) n =
    if length l ≤ width then
      if length l ≤ n then toByte [] else toByte (drop n l)
    else if width ≤ n then toByte []
    else toByte (drop n (take width l))

⊦ ∀pb pc s.
    parse (parsePair pb pc) s =
    case parse pb s of
      none → none
    | some (b, s') →
        case parse pc s' of
          none → none
        | some (c, s'') → some ((b, c), s'')

⊦ ∀pl pos.
    isChar (pl, pos) ⇔
    let pli ← destPlane pl in
    let posi ← destPosition pos in
    ¬(pli = 0) ∨ posi < 55296 ∨ 57343 < posi ∧ posi < 65534

OpenTheory package document generated by opentheory 1.2 (release 20140721)