Package char: Unicode characters

Information

Files

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

Defined Type Operator

• Data
  • Char
    • char

Defined Constants

• Data
  • Char
    • dest
    • destPlane
    • destPosition
    • invariant
    • mk
    • plane
    • position
    • random
    • UTF8
      • UTF8.decode
      • UTF8.encode
      • UTF8.encodeAscii
      • UTF8.encodeChar
        • UTF8.encodeChar.encode2
        • UTF8.encodeChar.encode3
        • UTF8.encodeChar.encode4
      • UTF8.isContinuationByte
      • UTF8.parse
      • UTF8.parseAscii
      • UTF8.parseChar
      • UTF8.parseMultibyte
        • UTF8.parseMultibyte.addContinuationByte
        • UTF8.parseMultibyte.parse2
        • UTF8.parseMultibyte.parse3
        • UTF8.parseMultibyte.parse4
      • UTF8.parseNatural
      • UTF8.reencode
      • UTF8.reencodeChar

Theorems

⊦ surjective random

⊦ finite universe

⊦ inverse UTF8.parseChar UTF8.encodeChar

⊦ strongInverse UTF8.parseChar UTF8.encodeChar

⊦ plane = destPlane ∘ dest

⊦ position = destPosition ∘ dest

⊦ UTF8.parseNatural = orelse UTF8.parseAscii UTF8.parseMultibyte

⊦ ∀a. mk (dest a) = a

⊦ ∀b. UTF8.reencode (UTF8.decode b) = b

⊦ ∀c. ∃r. random r = c

⊦ ∀c. plane c = destPlane (dest c)

⊦ ∀c. position c = destPosition (dest c)

⊦ ∀c. 1 ≤ length (UTF8.encodeChar c)

⊦ ∀c. UTF8.reencodeChar (right c) = UTF8.encodeChar c

⊦ ∀n. length (UTF8.encodeAscii n) = 1

⊦ ∀b. length (UTF8.decode b) ≤ length b

⊦ ∀b. UTF8.reencode (map left b) = b

⊦ ∀c. length c ≤ length (UTF8.encode c)

⊦ ∀c. 1 ≤ length (UTF8.reencodeChar c)

⊦ ∀c. length c ≤ length (UTF8.reencode c)

⊦ ∀b. UTF8.reencodeChar (left b) = b :: []

⊦ ∀n. UTF8.encodeAscii n = fromNatural n :: []

⊦ ∀n. length (UTF8.encodeChar.encode2 n) = 2

⊦ ∀n. length (UTF8.encodeChar.encode3 n) = 3

⊦ ∀c. UTF8.encode c = concat (map UTF8.encodeChar c)

⊦ ∀c. UTF8.decode (UTF8.encode c) = map right c

⊦ ∀c. UTF8.reencode (map right c) = UTF8.encode c

⊦ ∀c. UTF8.reencode c = concat (map UTF8.reencodeChar c)

⊦ UTF8.parse = orelse (map UTF8.parseChar right) (map any left)

⊦ ∀r. invariant r ⇔ dest (mk r) = r

⊦ ∀n. length (UTF8.encodeChar.encode4 n) = 4

⊦ ∀c. ∃n. invariant n ∧ c = mk n

⊦ finite { n. n | invariant n }

⊦ ∀c. plane c < 17

⊦ ∀b. UTF8.decode b = fst (toList (parse UTF8.parse (fromList b)))

⊦ ∀n b. apply UTF8.parseAscii (append (UTF8.encodeChar.encode2 n) b) = none

⊦ ∀n b. apply UTF8.parseAscii (append (UTF8.encodeChar.encode3 n) b) = none

⊦ ∀n b. apply UTF8.parseAscii (append (UTF8.encodeChar.encode4 n) b) = none

⊦ UTF8.parseChar =
  mapPartial UTF8.parseNatural
    (λn. if invariant n then some (mk n) else none)

⊦ ∀c₁ c₂. dest c₁ = dest c₂ ⇔ c₁ = c₂

⊦ ∀n. destPlane n = Bits.shiftRight n 16

⊦ ∀n. destPosition n = Bits.bound n 16

⊦ ∀x.
    UTF8.reencodeChar x =
    case x of left b → b :: [] | right c → UTF8.encodeChar c

⊦ image mk { n. n | invariant n } = universe

⊦ ∀n. invariant n ⇒ Bits.width n ≤ 21

⊦ UTF8.parseAscii =
  token (λb. if bit b 7 then none else some (toNatural b))

⊦ ∀c. ∃n. invariant n ∧ c = mk n ∧ dest c = n

⊦ ∀c. dest c = position c + Bits.shiftLeft (plane c) 16

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

⊦ ∀n. UTF8.isContinuationByte (or 128 (fromNatural (Bits.bound n 6)))

⊦ ∀c. position c < 65534

⊦ size universe = 1111998

⊦ ∀n b.
    n < 128 ⇒
    apply UTF8.parseAscii (append (UTF8.encodeAscii n) b) = some (n, b)

⊦ ∀c. dest c < 1114110

⊦ ∀n. destPlane n = 0 ⇔ n < 65536

⊦ ∀n. invariant n ⇒ n < 1114110

⊦ ∀b n.
    UTF8.parseMultibyte.addContinuationByte b n =
    if UTF8.isContinuationByte b then
      some (toNatural (and b 63) + Bits.shiftLeft n 6)
    else none

⊦ ∀b.
    UTF8.parseMultibyte.parse2 b =
    filter
      (foldN UTF8.parseMultibyte.addContinuationByte 0
         (toNatural (and b 31))) (λn. 128 ≤ n)

⊦ ∀b.
    UTF8.parseMultibyte.parse3 b =
    filter
      (foldN UTF8.parseMultibyte.addContinuationByte 1
         (toNatural (and b 15))) (λn. 2048 ≤ n)

⊦ ∀n m.
    UTF8.parseMultibyte.addContinuationByte
      (or 128 (fromNatural (Bits.bound n 6))) m =
    some (Bits.bound n 6 + Bits.shiftLeft m 6)

⊦ ∀b.
    UTF8.parseMultibyte.parse4 b =
    filter
      (foldN UTF8.parseMultibyte.addContinuationByte 2
         (toNatural (and b 7))) (λn. 65536 ≤ n)

⊦ ∀n b.
    128 ≤ n ∧ n < 2048 ⇒
    apply UTF8.parseMultibyte (append (UTF8.encodeChar.encode2 n) b) =
    some (n, b)

⊦ UTF8.parseMultibyte =
  sequence
    (token
       (λb.
          if bit b 6 then
            if bit b 5 then
              if bit b 4 then
                if bit b 3 then none
                else some (UTF8.parseMultibyte.parse4 b)
              else some (UTF8.parseMultibyte.parse3 b)
            else some (UTF8.parseMultibyte.parse2 b)
          else none))

⊦ ∀n b.
    65536 ≤ n ∧ Bits.width n ≤ 21 ⇒
    apply UTF8.parseMultibyte (append (UTF8.encodeChar.encode4 n) b) =
    some (n, b)

⊦ ∀n.
    UTF8.encodeChar.encode2 n =
    let n₁ ← Bits.shiftRight n 6 in
    let b₀ ← or 192 (fromNatural n₁) in
    let b₁ ← or 128 (fromNatural (Bits.bound n 6)) in
    b₀ :: b₁ :: []

⊦ ∀n b.
    2048 ≤ n ∧ n < 65536 ⇒
    apply UTF8.parseMultibyte (append (UTF8.encodeChar.encode3 n) b) =
    some (n, b)

⊦ UTF8.encodeChar =
  λc.
    let n ← dest c in
    if n < 128 then UTF8.encodeAscii n
    else if n < 2048 then UTF8.encodeChar.encode2 n
    else if n < 65536 then UTF8.encodeChar.encode3 n
    else UTF8.encodeChar.encode4 n

⊦ ∀c.
    UTF8.encodeChar c =
    let n ← dest c in
    if n < 128 then UTF8.encodeAscii n
    else if n < 2048 then UTF8.encodeChar.encode2 n
    else if n < 65536 then UTF8.encodeChar.encode3 n
    else UTF8.encodeChar.encode4 n

⊦ ∀n.
    UTF8.encodeChar.encode3 n =
    let n₁ ← Bits.shiftRight n 6 in
    let n₂ ← Bits.shiftRight n₁ 6 in
    let b₀ ← or 224 (fromNatural n₂) in
    let b₁ ← or 128 (fromNatural (Bits.bound n₁ 6)) in
    let b₂ ← or 128 (fromNatural (Bits.bound n 6)) in
    b₀ :: b₁ :: b₂ :: []

⊦ ∀n.
    UTF8.encodeChar.encode4 n =
    let n₁ ← Bits.shiftRight n 6 in
    let n₂ ← Bits.shiftRight n₁ 6 in
    let n₃ ← Bits.shiftRight n₂ 6 in
    let b₀ ← or 240 (fromNatural n₃) in
    let b₁ ← or 128 (fromNatural (Bits.bound n₂ 6)) in
    let b₂ ← or 128 (fromNatural (Bits.bound n₁ 6)) in
    let b₃ ← or 128 (fromNatural (Bits.bound n 6)) in
    b₀ :: b₁ :: b₂ :: b₃ :: []

⊦ ∀n.
    invariant n ⇔
    let pl ← destPlane n in
    let pos ← destPosition n in
    pl < 17 ∧ pos < 65534 ∧
    (pl = 0 ⇒ ¬(55296 ≤ pos ∧ pos < 57344) ∧ ¬(64976 ≤ pos ∧ pos < 65008))

⊦ ∀n.
    invariant n ⇔
    let pl ← destPlane n in
    let pos ← destPosition n in
    pos < 65534 ∧
    if ¬(pl = 0) then pl < 17
    else ¬(55296 ≤ pos ∧ pos < 57344) ∧ ¬(64976 ≤ pos ∧ pos < 65008)

⊦ ∀r.
    random r =
    let n₀ ← Uniform.random 1111998 r in
    let n₁ ← if n₀ < 55296 then n₀ else n₀ + 2048 in
    let n₂ ← if n₁ < 64976 then n₁ else n₁ + 32 in
    let pl ← n₂ div 65534 in
    let pos ← n₂ mod 65534 in
    let n ← pos + Bits.shiftLeft pl 16 in
    mk n

External Type Operators

• →
• bool
• Data
  • Byte
    • byte
  • List
    • list
  • Option
    • option
  • Pair
    • ×
  • Sum
    • +
• Number
  • Natural
    • natural
• Parser
  • parser
  • Stream
    • stream
• Probability
  • Random
    • random
• Set
  • set

External Constants

• =
• select
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • cond
    • ⊥
    • ⊤
  • Byte
    • <
    • and
    • bit
    • fromNatural
    • or
    • toNatural
    • width
    • Bits
      • Bits.compare
      • Bits.fromByte
      • Bits.toByte
  • List
    • ::
    • @
    • []
    • concat
    • length
    • map
    • nth
    • replicate
    • take
  • Option
    • case
    • map
    • none
    • some
  • Pair
    • ,
    • fst
    • snd
  • Sum
    • case
    • left
    • right
• Function
  • ∘
  • surjective
• Number
  • Natural
    • *
    • +
    • -
    • <
    • ≤
    • ↑
    • bit0
    • bit1
    • div
    • even
    • min
    • mod
    • suc
    • zero
    • Bits
      • Bits.and
      • Bits.bit
      • Bits.bound
      • Bits.cons
      • Bits.fromList
      • Bits.head
      • Bits.or
      • Bits.shiftLeft
      • Bits.shiftRight
      • Bits.width
    • Uniform
      • Uniform.random
• Parser
  • any
  • apply
  • filter
  • fold
    • fold.prs
  • foldN
  • inverse
  • map
  • mapPartial
  • orelse
  • parse
  • sequence
  • strongInverse
  • token
  • Stream
    • append
    • case
    • cons
    • eof
    • error
    • fromList
    • isProperSuffix
    • isSuffix
    • length
    • toList
• Set
  • ∅
  • cross
  • \
  • disjoint
  • finite
  • fromPredicate
  • image
  • insert
  • ∩
  • ∈
  • size
  • ⊆
  • ∪
  • universe

Assumptions

⊦ ⊤

⊦ Bits.head 1

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ length [] = 0

⊦ bit0 0 = 0

⊦ Bits.fromList [] = 0

⊦ concat [] = []

⊦ fromList [] = eof

⊦ ∀x. x ∈ universe

⊦ ∀t. t ⇒ t

⊦ ∀n. 0 ≤ n

⊦ ∀n. n ≤ n

⊦ ∀xs. isSuffix xs xs

⊦ ⊥ ⇔ ∀p. p

⊦ ∀x. ¬(x ∈ ∅)

⊦ ∀t. t ∨ ¬t

⊦ ∀m. ¬(m < 0)

⊦ ∀n. ¬(n < n)

⊦ ∀n. 0 < suc n

⊦ ∀n. n < suc n

⊦ (¬) = λp. p ⇒ ⊥

⊦ (∃) = λp. p ((select) 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 ∨ ⊤ ⇔ ⊤

⊦ ∀x. fromNatural (toNatural x) = x

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. 0 * n = 0

⊦ ∀m. m * 0 = 0

⊦ ∀n. 0 + n = n

⊦ ∀m. m + 0 = m

⊦ ∀m. m - 0 = m

⊦ ∀n. n - n = 0

⊦ ∀n. min n n = n

⊦ ∀k. Bits.bound 0 k = 0

⊦ ∀n. Bits.or 0 n = n

⊦ ∀k. Bits.shiftLeft 0 k = 0

⊦ ∀k. Bits.shiftRight 0 k = 0

⊦ ∀l. [] @ l = l

⊦ ∀f. map f [] = []

⊦ ∀f. map f none = none

⊦ ∀p. parse p eof = eof

⊦ ∀p. apply p eof = none

⊦ ∀p. apply p error = none

⊦ width = 8

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

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

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

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

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

⊦ ∀n. Bits.bit n 0 ⇔ Bits.head n

⊦ ∀m. m ↑ 0 = 1

⊦ ∀m. m * 1 = m

⊦ ∀m. 1 * m = m

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

⊦ ∀l. Bits.toByte l = fromNatural (Bits.fromList l)

⊦ ∀m n. m ≤ m + n

⊦ ∀n k. Bits.bound n k ≤ n

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

⊦ ∀x. size (insert x ∅) = 1

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

⊦ ∀w. Bits.bound (toNatural w) width = toNatural w

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

⊦ ∀m. m ≤ 0 ⇔ m = 0

⊦ ∀n. toNatural (fromNatural n) = Bits.bound n width

⊦ ∀l. toList (fromList l) = (l, ⊥)

⊦ ∀x. (fst x, snd x) = x

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

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

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

⊦ ∀b f. case b f none = b

⊦ ∀m n. ¬(n + m < m)

⊦ ∀n k. Bits.width (Bits.bound n k) ≤ k

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

⊦ ∀n. 0 < n ⇔ ¬(n = 0)

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

⊦ ∀f y. (let x ← y in f x) = f y

⊦ ∀x. ∃a b. x = (a, b)

⊦ ∀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 ⇒ m ≤ n

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

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

⊦ ∀n k. Bits.bound (Bits.shiftLeft n k) k = 0

⊦ ∀n k. Bits.shiftRight (Bits.bound n k) k = 0

⊦ ∀s t. finite s ⇒ finite (s \ t)

⊦ ∀f l. length (map f l) = length l

⊦ ∀f s. finite s ⇒ finite (image f s)

⊦ ∀p xs. length (parse p xs) ≤ length xs

⊦ ∀n. Bits.cons ⊥ n = 2 * n

⊦ ∀n. n ↑ 2 = n * n

⊦ ∀n. 2 * n = n + n

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

⊦ ∀w n. bit w n ⇔ Bits.bit (toNatural w) n

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

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

⊦ ∀n i. Bits.bit n i ⇒ i < Bits.width n

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

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

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

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

⊦ ∀f a. map f (some a) = some (f a)

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

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

⊦ ∀k. Bits.shiftLeft 1 k = 2 ↑ k

⊦ ∀f. surjective f ⇔ ∀y. ∃x. y = f x

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

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

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

⊦ ∀x y. x ∈ insert y ∅ ⇔ x = y

⊦ ∀a b. some a = some b ⇔ a = b

⊦ ∀h t. (h :: []) @ t = h :: t

⊦ ∀t₁ t₂. ¬t₁ ⇒ ¬t₂ ⇔ t₂ ⇒ t₁

⊦ ∀h t. Bits.fromList (h :: t) = Bits.cons h (Bits.fromList t)

⊦ ∀x y. x < y ⇔ toNatural x < toNatural y

⊦ ∀m n. m < n ⇒ m div n = 0

⊦ ∀m n. m < n ⇒ m mod n = m

⊦ ∀n₁ n₂. n₁ ≤ n₂ ⇒ Bits.width n₁ ≤ Bits.width n₂

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

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

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

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

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

⊦ ∀m n. m + n = m ⇔ n = 0

⊦ ∀k n. Bits.shiftLeft n k = 0 ⇔ n = 0

⊦ ∀n k. Bits.bound (Bits.bound n k) k = Bits.bound n k

⊦ ∀l₁ l₂. fromList (l₁ @ l₂) = append l₁ (fromList l₂)

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

⊦ ∀s t. disjoint s t ⇔ s ∩ t = ∅

⊦ ∀s t. finite t ∧ s ⊆ t ⇒ finite s

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

⊦ ∀n. finite { m. m | m < n }

⊦ ∀k. Bits.width (2 ↑ k - 1) = k

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

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

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

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

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

⊦ ∀w₁ w₂. and w₁ w₂ = fromNatural (Bits.and (toNatural w₁) (toNatural w₂))

⊦ ∀w₁ w₂. or w₁ w₂ = fromNatural (Bits.or (toNatural w₁) (toNatural w₂))

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

⊦ ∀m n. min m n = if m ≤ n then m else n

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

⊦ ∀n k. Bits.bound n k = n ⇔ Bits.width n ≤ k

⊦ ∀n k. Bits.shiftRight n k = 0 ⇔ Bits.width n ≤ k

⊦ ∀l₁ l₂. length (l₁ @ l₂) = length l₁ + length l₂

⊦ ∀s t. finite (s ∪ t) ⇔ finite s ∧ finite t

⊦ ∀s t. finite s ∧ finite t ⇒ finite (cross s t)

⊦ ∀p. (∀x. p x) ⇔ ∀a b. p (a, b)

⊦ ∀p. (∃x. p x) ⇔ ∃a b. p (a, b)

⊦ ∀m n. m ≤ n ⇔ ∃d. n = m + d

⊦ ∀n i. i < n ⇒ ∃r. Uniform.random n r = i

⊦ ∀n. Bits.cons ⊤ n = 1 + 2 * n

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

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

⊦ ∀n k. Bits.shiftLeft n k = 2 ↑ k * n

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

⊦ ∀n k. Bits.bound n k + Bits.shiftLeft (Bits.shiftRight n k) k = n

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

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

⊦ ∀n. size { m. m | m < n } = n

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

⊦ ∀n k. Bits.width n ≤ k ⇔ n < 2 ↑ k

⊦ ∀x y z. x = y ∧ y = z ⇒ x = z

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

⊦ ∀n k i. Bits.bit n (k + i) ⇔ Bits.bit (Bits.shiftRight n k) i

⊦ ∀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 k₁ k₂.
    Bits.shiftRight n (k₁ + k₂) = Bits.shiftRight (Bits.shiftRight n k₁) k₂

⊦ ∀n j k. Bits.bound (Bits.bound n j) k = Bits.bound n (min j k)

⊦ ∀m n p. m + n = m + p ⇔ n = p

⊦ ∀p m n. m + p = n + p ⇔ m = n

⊦ ∀m n p. n + m < p + m ⇔ n < p

⊦ ∀m n p. m + n ≤ m + p ⇔ n ≤ p

⊦ ∀m n p. n + m ≤ p + m ⇔ n ≤ p

⊦ ∀k n₁ n₂. Bits.shiftLeft n₁ k ≤ Bits.shiftLeft n₂ k ⇔ n₁ ≤ n₂

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

⊦ ∀n₁ n₂ k. Bits.bound (n₁ + Bits.shiftLeft n₂ k) k = Bits.bound n₁ k

⊦ ∀m n p. m < n ∧ n ≤ p ⇒ m < p

⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p

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

⊦ ∀s t. s ⊆ t ⇔ ∀x. x ∈ s ⇒ x ∈ t

⊦ ∀s t. (∀x. x ∈ s ⇔ x ∈ t) ⇔ s = t

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

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

⊦ ∀m n. m + n = 0 ⇔ m = 0 ∧ n = 0

⊦ ∀l i. Bits.bit (Bits.fromList l) i ⇔ i < length l ∧ nth l i

⊦ ∀xs ys e. toList xs = (ys, e) ⇒ length xs = length ys

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

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

⊦ ∀n k. Bits.and n (2 ↑ k - 1) = Bits.bound n k

⊦ ∀p x. x ∈ { y. y | p y } ⇔ p x

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

⊦ ∀k w₁ w₂. bit (or w₁ w₂) k ⇔ bit w₁ k ∨ bit w₂ k

⊦ ∀n i k. Bits.bit (Bits.bound n k) i ⇔ i < k ∧ Bits.bit n i

⊦ ∀m n i. Bits.bit (Bits.or m n) i ⇔ Bits.bit m i ∨ Bits.bit n i

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

⊦ ∀m n k.
    Bits.bound (Bits.and m n) k =
    Bits.and (Bits.bound m k) (Bits.bound n k)

⊦ ∀m n k.
    Bits.bound (Bits.or m n) k = Bits.or (Bits.bound m k) (Bits.bound n k)

⊦ ∀n j k. Bits.width n ≤ j + k ⇒ Bits.width (Bits.shiftRight n k) ≤ j

⊦ ∀n₁ n₂ k.
    Bits.shiftRight (n₁ + Bits.shiftLeft n₂ k) k =
    Bits.shiftRight n₁ k + n₂

⊦ ∀xs. xs = error ∨ xs = eof ∨ ∃x xt. xs = cons x xt

⊦ ∀s t x. x ∈ s ∩ t ⇔ x ∈ s ∧ x ∈ t

⊦ ∀s t x. x ∈ s ∪ t ⇔ x ∈ s ∨ x ∈ t

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

⊦ ∀p. (∀xs. (∀ys. isProperSuffix ys xs ⇒ p ys) ⇒ p xs) ⇒ ∀xs. p xs

⊦ ∀s t x. x ∈ s \ t ⇔ x ∈ s ∧ ¬(x ∈ t)

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

⊦ ∀s t. finite s ∧ finite t ⇒ size (cross s t) = size s * size t

⊦ ∀p. p [] ∧ (∀h t. p t ⇒ p (h :: t)) ⇒ ∀l. p l

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

⊦ ∀w₁ w₂. (∀i. i < width ⇒ (bit w₁ i ⇔ bit w₂ i)) ⇒ w₁ = w₂

⊦ ∀n k i. Bits.bit (Bits.shiftLeft n k) i ⇔ k ≤ i ∧ Bits.bit n (i - k)

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

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

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

⊦ ∀y s f. y ∈ image f s ⇔ ∃x. y = f x ∧ x ∈ s

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

⊦ ∀s t. finite s ∧ t ⊆ s ⇒ size (s \ t) = size s - size t

⊦ ∀p₁ p₂ xs.
    apply (orelse p₁ p₂) xs =
    case apply p₁ xs of none → apply p₂ xs | some yys → some yys

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

⊦ ∀x y s t. (x, y) ∈ cross s t ⇔ x ∈ s ∧ y ∈ t

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

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

⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)

⊦ ∀a b n. ¬(n = 0) ⇒ (a * n + b) div n = a + b div n

⊦ ∀m n j k.
    Bits.width (Bits.bound m k + Bits.shiftLeft n k) ≤ j + k ⇔
    Bits.width n ≤ j

⊦ ∀l xs ys e. toList (append l xs) = (l @ ys, e) ⇔ toList xs = (ys, e)

⊦ ∀s t. finite s ∧ finite t ∧ disjoint s t ⇒ size (s ∪ t) = size s + size t

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

⊦ ∀x xs. toList (cons x xs) = let (l, e) ← toList xs in (x :: l, e)

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

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