Package char-def: Definition of Unicode characters

Information

name	char-def
version	1.93
description	Definition of Unicode characters
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2012-12-10
requires	bool byte natural pair word16
show	Data.Bool Data.Byte Data.Char Data.Pair Data.Word16 Number.Natural Probability.Random

Files

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

Defined Type Operators

Data
- Char
  - char
  - plane
  - position

Defined Constants

Data
- Char
  - destChar
  - destPlane
  - destPosition
  - fromRandom
  - isChar
  - isPlane
  - isPosition
  - mkChar
  - mkPlane
  - mkPosition
  - planeFromRandom
  - positionFromRandom

Theorems

⊦ ∀p. isPosition p

⊦ ∀a. mkChar (destChar a) = a

⊦ ∀a. mkPlane (destPlane a) = a

⊦ ∀a. mkPosition (destPosition a) = a

⊦ ∀r. destPosition (mkPosition r) = r

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

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

⊦ ∀p. isPlane p ⇔ p < 17

⊦ ∀r.
positionFromRandom r = let (w, r') ← fromRandom r in (mkPosition w, r')

⊦ ∀r.
planeFromRandom r =
let (n, r') ← Uniform.fromRandom 17 r in (mkPlane (fromNatural n), r')

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

⊦ ∀r.
    fromRandom r =
    let (pl, r') ← planeFromRandom r in
    let pli ← destPlane pl in
    let (pos, r'') ←
        if ¬(pli = 0) then positionFromRandom r'
        else
          let (n, r''') ← Uniform.fromRandom 63486 r' in
          let n' ← if n < 55296 then n else n + 2048 in
          (mkPosition (fromNatural n'), r''') in
    (mkChar (pl, pos), r'')

External Type Operators

→
bool
Data
- Byte
  - byte
- Pair
  - ×
- Word16
  - word16
Number
- Natural
  - natural
Probability
- Random
  - random

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- Byte
  - <
  - fromNatural
  - modulus
  - toNatural
  - width
- Pair
  - ,
  - fst
  - snd
- Word16
  - <
  - fromNatural
  - fromRandom
Number
- Natural
  - *
  - +
  - <
  - ≤
  - ↑
  - bit0
  - bit1
  - div
  - even
  - mod
  - suc
  - zero
  - Uniform
    - Uniform.fromRandom

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ bit0 0 = 0

⊦ ∀t. t ⇒ t

⊦ ∀n. 0 ≤ n

⊦ ⊥ ⇔ ∀p. p

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ ⊥

⊦ (∃) = λp. p ((select) p)

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

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

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

⊦ ∀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 ∨ ⊤ ⇔ ⊤

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. 0 * n = 0

⊦ ∀m. m * 0 = 0

⊦ ∀n. 0 + n = n

⊦ ∀m. m + 0 = m

⊦ modulus = 2 ↑ width

⊦ width = 8

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

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

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

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

⊦ ∀m. m ↑ 0 = 1

⊦ ∀m. m * 1 = m

⊦ ∀m. 1 * m = m

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

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

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

⊦ ∀m. m ≤ 0 ⇔ m = 0

⊦ ∀n. toNatural (fromNatural n) = n mod modulus

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

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

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

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

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

⊦ ∀n. 2 * n = n + n

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

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

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

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

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

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

⊦ ∀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. 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 q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

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

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

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

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

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

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

⊦ ∀x y. fromNatural x = fromNatural y ⇔ x mod modulus = y mod modulus

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

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

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

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

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

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

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

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