Package char-thm: Properties of Unicode characters
Information
| name | char-thm |
| version | 1.17 |
| description | Properties of Unicode characters |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2014-11-01 |
| checksum | c42ad7b2ea4a581bd21ea5559ab740922febd8fd |
| requires | bool char-def pair |
| show | Data.Bool Data.Byte Data.Char Data.Pair Data.Word16 |
Files
- Package tarball char-thm-1.17.tgz
- Theory source file char-thm.thy (included in the package tarball)
Theorems
⊦ ∀pos. ∃w. pos = mkPosition w
⊦ ∀pl. ∃b. isPlane b ∧ pl = mkPlane b
⊦ ∀c1 c2. destChar c1 = destChar c2 ⇔ c1 = c2
⊦ ∀pl1 pl2. destPlane pl1 = destPlane pl2 ⇔ pl1 = pl2
⊦ ∀pos1 pos2. destPosition pos1 = destPosition pos2 ⇔ pos1 = pos2
⊦ ∀pos. ∃w. pos = mkPosition w ∧ destPosition pos = w
⊦ ∀pl. ∃b. isPlane b ∧ pl = mkPlane b ∧ destPlane pl = b
⊦ ∀c. ∃pl pos. isChar (pl, pos) ∧ c = mkChar (pl, pos)
⊦ ∀c.
∃pl pos.
isChar (pl, pos) ∧ c = mkChar (pl, pos) ∧ destChar c = (pl, pos)
External Type Operators
- →
- bool
- Data
- Byte
- byte
- Char
- char
- plane
- position
- Pair
- ×
- Word16
- word16
- Byte
External Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ⊤
- Char
- destChar
- destPlane
- destPosition
- isChar
- isPlane
- mkChar
- mkPlane
- mkPosition
- Pair
- ,
- fst
- snd
- Bool
Assumptions
⊦ ⊤
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀a. mkChar (destChar a) = a
⊦ ∀a. mkPlane (destPlane a) = a
⊦ ∀a. mkPosition (destPosition a) = a
⊦ ∀r. destPosition (mkPosition r) = r
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀x. (fst x, snd x) = x
⊦ ∀r. isPlane r ⇔ destPlane (mkPlane r) = r
⊦ ∀r. isChar r ⇔ destChar (mkChar r) = r
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q